License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.597
URN: urn:nbn:de:0030-drops-54418
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5441/
Go to the corresponding LIPIcs Volume Portal

Kierónski, Emanuel ; Kuusisto, Antti

Uniform One-Dimensional Fragments with One Equivalence Relation

pdf-format:
37.pdf (0.5 MB)

Abstract

The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.

BibTeX - Entry

@InProceedings{kiernski_et_al:LIPIcs:2015:5441,
  author =	{Emanuel Kier{\'o}nski and Antti Kuusisto},
  title =	{{Uniform One-Dimensional Fragments with One Equivalence Relation}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{597--615},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5441},
  URN =		{urn:nbn:de:0030-drops-54418},
  doi =		{10.4230/LIPIcs.CSL.2015.597},
  annote =	{Keywords: two-variable logic, uniform one-dimensional fragments, complexity, expressivity, equivalence relations}
}

Keywords: two-variable logic, uniform one-dimensional fragments, complexity, expressivity, equivalence relations
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

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