LIPIcs.STACS.2013.317.pdf
- Filesize: 0.7 MB
- 12 pages
Document
FO^2 with one transitive relation is decidable
Authors
-
Part of:
Volume:
30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution-NoDerivs 3.0 Unported license
- Publication Date: 2013-02-26
Cite AsGet BibTex
Wieslaw Szwast and Lidia Tendera. FO^2 with one transitive relation is decidable. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 317-328, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.STACS.2013.317
https://doi.org/10.4230/LIPIcs.STACS.2013.317
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.
Keywords
- classical decision problem
- two-variable first-order logic
- decidability
- computational complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads