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.
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 language | English |
|---|---|
| DOIs | |
| Publication status | Published - 2 Jul 2021 |
| Event | 48th International Colloquium on Automata, Languages, and Programming : ICALP 2021 - Duration: 12 Jul 2021 → 16 Jul 2021 |
Conference
| Conference | 48th International Colloquium on Automata, Languages, and Programming |
|---|---|
| Period | 12/07/21 → 16/07/21 |