Adding Transitivity and Counting to the Fluted Fragment

Ian Pratt-Hartmann, Lidia Tendera

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We study the impact of adding both counting quantifiers and a single transitive relation to the fluted fragment - a fragment of first-order logic originating in the work of W.V.O. Quine. The resulting formalism can be viewed as a multi-variable, non-guarded extension of certain systems of description logic featuring number restrictions and transitive roles, but lacking role-inverses. We establish the finite model property for our logic, and show that the satisfiability problem for its k-variable sub-fragment is in (k+1)-NExpTime. We also derive ExpSpace-hardness of the satisfiability problem for the two-variable, fluted fragment with one transitive relation (but without counting quantifiers), and prove that, when a second transitive relation is allowed, both the satisfiability and the finite satisfiability problems for the two-variable fluted fragment with counting quantifiers become undecidable.
Original languageEnglish
Title of host publication31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages32:1--32:22
Number of pages22
ISBN (Print)978-3-95977-264-8
DOIs
Publication statusPublished - 11 Feb 2023

Publication series

NameLeibniz International Proceedings in Informatics
PublisherSchloss Dagstuhl -- Leibniz-Zentrum für Informatik
ISSN (Print)1868-8969

Keywords

  • fluted logic
  • transitivity
  • counting
  • satisfiability
  • decidability
  • complexity

Fingerprint

Dive into the research topics of 'Adding Transitivity and Counting to the Fluted Fragment'. Together they form a unique fingerprint.

Cite this