Back to Search Start Over

FO^2 with one transitive relation is decidable

Authors :
Wieslaw Szwast and Lidia Tendera
Szwast, Wieslaw
Tendera, Lidia
Wieslaw Szwast and Lidia Tendera
Szwast, Wieslaw
Tendera, Lidia
Publication Year :
2013

Abstract

We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.

Details

Database :
OAIster
Notes :
application/pdf, English
Publication Type :
Electronic Resource
Accession number :
edsoai.on1358719981
Document Type :
Electronic Resource
Full Text :
https://doi.org/10.4230.LIPIcs.STACS.2013.317