On the satisfiability problem for fragments of the two-variable logic with one transitive relation

2018/04/25 by Szwast, Wiesław, Tendera, Lidia
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1804.09447

Abstract

We study the satisfiability problem for the two-variable first-order logic over structures with one transitive relation. % We show that the problem is decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model nor the tree model property, to show decidability we introduce novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation, hence contrary to our previous claim, [FO² with one transitive relation is decidable, STACS 2013: 317-328], the status of the latter problem remains open.

Related

• The Fluted Fragment with Transitivity
• Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees
• On Generalizing Decidable Standard Prefix Classes of First-Order Logic
• Order-Invariance of Two-Variable Logic is Decidable
• Extending Two-Variable Logic on Trees