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.ICALP.2018.133
URN: urn:nbn:de:0030-drops-91375
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9137/
Go to the corresponding LIPIcs Volume Portal

Kuske, Dietrich ; Schweikardt, Nicole

Gaifman Normal Forms for Counting Extensions of First-Order Logic

pdf-format:
LIPIcs-ICALP-2018-133.pdf (0.5 MB)

Abstract

We consider the extension of first-order logic FO by unary counting quantifiers and generalise the notion of Gaifman normal form from FO to this setting. For formulas that use only ultimately periodic counting quantifiers, we provide an algorithm that computes equivalent formulas in Gaifman normal form. We also show that this is not possible for formulas using at least one quantifier that is not ultimately periodic.
Now let d be a degree bound. We show that for any formula phi with arbitrary counting quantifiers, there is a formula gamma in Gaifman normal form that is equivalent to phi on all finite structures of degree <= d. If the quantifiers of phi are decidable (decidable in elementary time, ultimately periodic), gamma can be constructed effectively (in elementary time, in worst-case optimal 3-fold exponential time).
For the setting with unrestricted degree we show that by using our Gaifman normal form for formulas with only ultimately periodic counting quantifiers, a known fixed-parameter tractability result for FO on classes of structures of bounded local tree-width can be lifted to the extension of FO with ultimately periodic counting quantifiers (a logic equally expressive as FO+MOD, i.e., first-oder logic with modulo-counting quantifiers).

BibTeX - Entry

@InProceedings{kuske_et_al:LIPIcs:2018:9137,
  author =	{Dietrich Kuske and Nicole Schweikardt},
  title =	{{Gaifman Normal Forms for Counting Extensions of First-Order Logic}},
  booktitle =	{45th International Colloquium on Automata, Languages, and  Programming (ICALP 2018)},
  pages =	{133:1--133:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Ioannis Chatzigiannakis and Christos Kaklamanis and D{\'a}niel Marx and Donald Sannella},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9137},
  URN =		{urn:nbn:de:0030-drops-91375},
  doi =		{10.4230/LIPIcs.ICALP.2018.133},
  annote =	{Keywords: Finite model theory, Gaifman locality, modulo-counting quantifiers, fixed parameter tractable model-checking}
}

Keywords: Finite model theory, Gaifman locality, modulo-counting quantifiers, fixed parameter tractable model-checking
Collection: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)
Issue Date: 2018
Date of publication: 04.07.2018

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