Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Kieronski, Emanuel http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-32415
URL:

Decidability Issues for Two-Variable Logics with Several Linear Orders

pdf-format:


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 =		{http://dx.doi.org/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
Seminar: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue date: 2011
Date of publication: 2011


DROPS-Home | Fulltext Search | Imprint Published by LZI