Adding Transitivity and Counting to the Fluted Fragment
| Autor: | Pratt-Hartmann, Ian, Tendera, Lidia |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | Pratt-Hartmann, I & Tendera, L 2023, Adding Transitivity and Counting to the Fluted Fragment . in 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) . Leibniz International Proceedings in Informatics, Schloss Dagstuhl-Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 32:1--32:22 . https://doi.org/10.4230/LIPIcs.CSL.2023.32 |
| DOI: | 10.4230/LIPIcs.CSL.2023.32 |
| Popis: | 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. LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 32:1-32:22 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|