The Fluted Fragment with Transitivity

Authors Ian Pratt-Hartmann , Lidia Tendera



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.18.pdf
  • Filesize: 0.69 MB
  • 15 pages

Document Identifiers

Author Details

Ian Pratt-Hartmann
  • University of Warsaw, Poland
  • University of Opole, Poland
  • University of Manchester, UK
Lidia Tendera
  • University of Opole, Poland

Cite AsGet BibTex

Ian Pratt-Hartmann and Lidia Tendera. The Fluted Fragment with Transitivity. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.MFCS.2019.18

Abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Finite Model Theory
Keywords
  • First-Order logic
  • Decidability
  • Satisfiability
  • Transitivity
  • Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998. Google Scholar
  2. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. Google Scholar
  3. E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997. Google Scholar
  4. D. Danielski and E. Kieron̈ski. Finite Satisfiability of Unary Negation Fragment with Transitivity. In Proceedings of MFCS 2019, volume 138, pages 17:1-17:15, 2019. Google Scholar
  5. E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  6. A. Herzig. A new decidable fragment of first order logic. In Abstracts of the 3rd Logical Biennial Summer School and Conference in Honour of S. C.Kleene, June 1990. Google Scholar
  7. Y. Kazakov and I. Pratt-Hartmann. A note on the complexity of the satisfiability problem for graded modal logic. In Logic in Computer Science, pages 407-416. IEEE, 2009. Google Scholar
  8. E. Kieroński, J. Michaliszyn, I. Pratt-Hartmann, and L. Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal on Computing, 43(3):1012-1063, 2014. Google Scholar
  9. E. Kieroński and M. Otto. Small Substructures and Decidability Issues for First-Order Logic with Two Variables. Journal of Symbolic Logic, 77:729-765, 2012. Google Scholar
  10. E. Kieroński and L. Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In Logic in Computer Science, pages 123-132. IEEE, 2009. Google Scholar
  11. R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6:467-480, 1980. Google Scholar
  12. A. Noah. Predicate-functors and the limits of decidability in logic. Notre Dame Journal of Formal Logic, 21(4):701-707, 1980. Google Scholar
  13. I. Pratt-Hartmann. Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable. Mathematical Logic Quarterly, 64(3):218-248, 2018. Google Scholar
  14. I. Pratt-Hartmann, W. Szwast, and L. Tendera. Quine’s fluted fragment is non-elementary. In 25th EACSL Annual Conference on Computer Science Logic, CSL, volume 62 of LIPIcs, pages 39:1-39:21. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  15. I. Pratt-Hartmann, W. Szwast, and L. Tendera. The fluted fragment revisited. Journal of Symbolic Logic, 2019. (Forthcoming). Google Scholar
  16. I. Pratt-Hartmann and L. Tendera. The fluted fragment with transitivity. ArXiv, 2019. extended version of MFCS'19 paper. URL: https://arxiv.org/abs/1906.09131.
  17. W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 61(2):608-620, 1996. Google Scholar
  18. W. C. Purdy. Complexity and nicety of fluted logic. Studia Logica, 71:177-198, 2002. Google Scholar
  19. W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62. University of Vienna, 1969. Google Scholar
  20. W. V. Quine. The variable. In The Ways of Paradox, pages 272-282. Harvard University Press, revised and enlarged edition, 1976. Google Scholar
  21. S. Schmitz. Complexity hierarchies beyond Elementary. ACM Transactions on Computation Theory, 8(1:3):1-36, 2016. Google Scholar
  22. D. Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27:477, 1962. Google Scholar
  23. W. Szwast and L. Tendera. On the satisfiability problem for fragments of the two-variable logic with one transitive relation. Journal of Logic and Computation, 2019. Forthcoming. Google Scholar
  24. L. Tendera. Decidability frontier for fragments of first-order logic with transitivity. In Proceedings of the 31st International Workshop on Description Logics co-located with 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), 2018. URL: http://ceur-ws.org/Vol-2211/paper-02.pdf.
  25. M. Vardi. On the complexity of bounded-variable queries. In Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 266-276, 1995. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail