10.4230/LIPICS.CSL.2011.337
Kieronski, Emanuel
Emanuel
Kieronski
Decidability Issues for Two-Variable Logics with Several Linear Orders
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
two-variable logic
linear orders
guarded fragment
decidability
Bezem, Marc
Marc
Bezem
2011
2011-08-31
2011-08-31
2011-08-31
en
urn:nbn:de:0030-drops-32415
10.4230/LIPIcs.CSL.2011
978-3-939897-32-3
1868-8969
10.4230/LIPIcs.CSL.2011
LIPIcs, Volume 12, CSL 2011
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
2013
12
27
337
351
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Bezem, Marc
Marc
Bezem
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
12
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
15 pages
749013 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
We show that the satisfiability and the finite satisfiability problems for two-variable logic, FO2, over the class of structures with three linear orders, are undecidable. This sharpens an earlier result that FO2 with eight linear orders is undecidable. The theorem holds for a restricted case in which linear orders are the only non-unary relations. Recently, a contrasting result has been shown, that the finite satisfiability problem for FO2 with two linear orders and with no additional non-unary relations is decidable. We observe that our proof can be adapted to some interesting fragments of FO2, in particular it works for the two-variable guarded fragment, GF2, even if the order relations are used only as guards. Finally, we show that GF2 with an arbitrary number of linear orders which can be used only as guards becomes decidable if except linear orders only unary relations are allowed.
LIPIcs, Vol. 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, pages 337-351