License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2021.141
URN: urn:nbn:de:0030-drops-142101
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14210/
Go to the corresponding LIPIcs Volume Portal

Pratt-Hartmann, Ian

Fluted Logic with Counting

pdf-format:
LIPIcs-ICALP-2021-141.pdf (0.8 MB)

Abstract

The fluted fragment is a fragment of first-order logic in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that the fluted fragment possesses the finite model property. In this paper, we extend the fluted fragment by the addition of counting quantifiers. We show that the resulting logic retains the finite model property, and that the satisfiability problem for its (m+1)-variable sub-fragment is in m-NExpTime for all positive m. We also consider the satisfiability and finite satisfiability problems for the extension of any of these fragments in which the fluting requirement applies only to sub-formulas having at least three free variables.

BibTeX - Entry

@InProceedings{pratthartmann:LIPIcs.ICALP.2021.141,
  author =	{Pratt-Hartmann, Ian},
  title =	{{Fluted Logic with Counting}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{141:1--141:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14210},
  URN =		{urn:nbn:de:0030-drops-142101},
  doi =		{10.4230/LIPIcs.ICALP.2021.141},
  annote =	{Keywords: Fluted fragment, counting quantifiers, satisfiability, complexity}
}

Keywords: Fluted fragment, counting quantifiers, satisfiability, complexity
Collection: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)
Issue Date: 2021
Date of publication: 02.07.2021

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