The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable.
arXiv: Logic in Computer Science(2017)
摘要
We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be interpreted as a partial order.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络