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.
@InProceedings{pratthartmann_et_al:LIPIcs.CSL.2023.32, author = {Pratt-Hartmann, Ian and Tendera, Lidia}, title = {{Adding Transitivity and Counting to the Fluted Fragment}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {32:1--32:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.32}, URN = {urn:nbn:de:0030-drops-174933}, doi = {10.4230/LIPIcs.CSL.2023.32}, annote = {Keywords: fluted logic, transitivity, counting, satisfiability, decidability, complexity} }
Feedback for Dagstuhl Publishing