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.MFCS.2019.16
URN: urn:nbn:de:0030-drops-109608
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10960/
Go to the corresponding LIPIcs Volume Portal

Kieronski, Emanuel

One-Dimensional Guarded Fragments

pdf-format:
LIPIcs-MFCS-2019-16.pdf (0.5 MB)

Abstract

We call a first-order formula one-dimensional if every maximal block of existential (or universal) quantifiers in it leaves at most one variable free. We consider the one-dimensional restrictions of the guarded fragment, GF, and the tri-guarded fragment, TGF, the latter being a recent extension of GF in which quantification for subformulas with at most two free variables need not be guarded, and which thus may be seen as a unification of GF and the two-variable fragment, FO^2. We denote the resulting formalisms, resp., GF_1, and TGF_1. We show that GF_1 has an exponential model property and NExpTime-complete satisfiability problem (that is, it is easier than full GF). For TGF_1 we show that it is decidable, has the finite model property, and its satisfiability problem is 2-ExpTime-complete (NExpTime-complete in the absence of equality). All the above-mentioned results are obtained for signatures with no constants. We finally discuss the impact of their addition, observing that constants do not spoil the decidability but increase the complexity of the satisfiability problem.

BibTeX - Entry

@InProceedings{kieronski:LIPIcs:2019:10960,
  author =	{Emanuel Kieronski},
  title =	{{One-Dimensional Guarded Fragments}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{16:1--16:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Peter Rossmanith and Pinar Heggernes and Joost-Pieter Katoen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10960},
  URN =		{urn:nbn:de:0030-drops-109608},
  doi =		{10.4230/LIPIcs.MFCS.2019.16},
  annote =	{Keywords: guarded fragment, two-variable logic, satisfiability, finite model property}
}

Keywords: guarded fragment, two-variable logic, satisfiability, finite model property
Collection: 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Issue Date: 2019
Date of publication: 20.08.2019

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