6533b832fe1ef96bd129ad22
RESEARCH PRODUCT
On the satisfiability problem for fragments of two-variable logic with one transitive relation
Wiesław SzwastLidia Tenderasubject
Transitive relationLogic010102 general mathematics0102 computer and information sciences01 natural sciencesTheoretical Computer ScienceCombinatoricsVariable (computer science)Arts and Humanities (miscellaneous)010201 computation theory & mathematicsHardware and Architecture0101 mathematicsBoolean satisfiability problemSoftwareMathematicsdescription
Abstract We study the satisfiability problem for 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 property nor the tree model property, to show decidability we introduce a 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$^2$ with one transitive relation is decidable, STACS 2013: 317-328], the status of the latter problem remains open.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2019-07-30 | Journal of Logic and Computation |