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.2012.396
URN: urn:nbn:de:0030-drops-36860
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3686/
Go to the corresponding LIPIcs Volume Portal

Kieronski, Emanuel ; Michaliszyn, Jakub

Two-Variable Universal Logic with Transitive Closure

pdf-format:
32.pdf (0.5 MB)

Abstract

We prove that the satisfiability problem for the two-variable, universal fragment of first-order logic with constants (or, alternatively phrased, for the Bernays-Schönfinkel class with two universally quantified variables) remains decidable after augmenting the fragment by the transitive closure of a single binary relation. We give a 2-NExpTime-upper bound and a 2-ExpTime-lower bound for the complexity of the problem. We also study the cases in which the number of constants is restricted. It appears that with two constants the considered fragment has the finite model property and NExpTime-complete satisfiability problem. Adding a third constant does not change the complexity but allows to construct infinity axioms. A fourth constant lifts the lower complexity bound to TwoExpTime. Finally, we observe that we are close to the border between decidability and undecidability: adding a third variable or the transitive closure of a second binary relation lead to undecidability.

BibTeX - Entry

@InProceedings{kieronski_et_al:LIPIcs:2012:3686,
  author =	{Emanuel Kieronski and Jakub Michaliszyn},
  title =	{{Two-Variable Universal Logic with Transitive Closure}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{396--410},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3686},
  URN =		{urn:nbn:de:0030-drops-36860},
  doi =		{10.4230/LIPIcs.CSL.2012.396},
  annote =	{Keywords: two-variable logic, transitive closure, decidability}
}

Keywords: two-variable logic, transitive closure, decidability
Collection: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 03.09.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI