License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.337
URN: urn:nbn:de:0030-drops-32415
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3241/
Kieronski, Emanuel
Decidability Issues for Two-Variable Logics with Several Linear Orders
Abstract
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.
BibTeX - Entry
@InProceedings{kieronski:LIPIcs:2011:3241,
author = {Emanuel Kieronski},
title = {{Decidability Issues for Two-Variable Logics with Several Linear Orders}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {337--351},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Marc Bezem},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3241},
URN = {urn:nbn:de:0030-drops-32415},
doi = {10.4230/LIPIcs.CSL.2011.337},
annote = {Keywords: two-variable logic, linear orders, guarded fragment, decidability}
}
Keywords: |
|
two-variable logic, linear orders, guarded fragment, decidability |
Collection: |
|
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL |
Issue Date: |
|
2011 |
Date of publication: |
|
31.08.2011 |