Fluted Logic with Counting

Research output: Contribution to conferencePaperpeer-review

44 Downloads (Pure)

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.
Original languageEnglish
DOIs
Publication statusPublished - 2 Jul 2021
Event48th International Colloquium on Automata, Languages, and Programming : ICALP 2021 -
Duration: 12 Jul 202116 Jul 2021

Conference

Conference48th International Colloquium on Automata, Languages, and Programming
Period12/07/2116/07/21

Fingerprint

Dive into the research topics of 'Fluted Logic with Counting'. Together they form a unique fingerprint.

Cite this