Document Open Access Logo

Adding Transitivity and Counting to the Fluted Fragment

Authors Ian Pratt-Hartmann, Lidia Tendera

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2023.32.pdf
  • Filesize: 0.79 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • fluted logic
  • transitivity
  • counting
  • satisfiability
  • decidability
  • complexity

Metrics

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

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.

Cite As Get BibTex

Ian Pratt-Hartmann and Lidia Tendera. Adding Transitivity and Counting to the Fluted Fragment. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.32

Author Details

Ian Pratt-Hartmann
  • Department of Computer Science, University of Manchester, UK
  • Institute of Computer Science, University of Opole, Poland
Lidia Tendera
  • Institute of Computer Science, University of Opole, Poland

Funding

This work was supported by the Polish NCN, grant number 2018/31/B/ST6/03662.

References

  1. Bartosz Bednarczyk. Exploiting forwardness: Satisfiability and query-entailment in forward guarded fragment. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, editors, Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, volume 12678 of Lecture Notes in Computer Science, pages 179-193. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-75775-5_13.
  2. Bartosz Bednarczyk, Emanuel Kieroński, and Piotr Witkowski. Completing the picture: Complexity of graded modal logics with converse. Theory Pract. Log. Program., 21(4):493-520, 2021. URL: https://doi.org/10.1017/S1471068421000065.
  3. Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 112:1-112:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.112.
  4. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  5. Diego Calvanese, Thomas Eiter, and Magdalena Ortiz. Answering regular path queries in expressive description logics via alternating tree-automata. Information and Computation, 237:12-55, 2014. URL: https://doi.org/10.1016/j.ic.2014.04.002.
  6. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  7. Daniel Danielski and Emanuel Kieroński. Unary negation fragment with equivalence relations has the finite model property. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 285-294. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209205.
  8. Daniel Danielski and Emanuel Kieroński. Finite satisfiability of unary negation fragment with transitivity. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 17:1-17:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.17.
  9. Thomas Eiter, Magdalena Ortiz, and Mantas Simkus. Conjunctive query answering in the description logic SH using knots. Journal of Computer and System Sciences, 78(1):47-85, 2012. URL: https://doi.org/10.1016/j.jcss.2011.02.012.
  10. Birte Glimm, Ian Horrocks, and Ulrike Sattler. Unions of conjunctive queries in SHOQ. In Gerhard Brewka and Jérôme Lang, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference, KR 2008, Sydney, Australia, September 16-19, 2008, pages 252-262. AAAI Press, 2008. URL: http://www.aaai.org/Library/KR/2008/kr08-025.php.
  11. Birte Glimm, Carsten Lutz, Ian Horrocks, and Ulrike Sattler. Conjunctive query answering for the description logic SHIQ. J. Artif. Intell. Res., 31:157-204, 2008. URL: https://doi.org/10.1613/jair.2372.
  12. Tomasz Gogacz, Víctor Gutiérrez-Basulto, Yazmín Ibáñez-García, Jean Christoph Jung, and Filip Murlak. On finite and unrestricted query entailment beyond SQ with number restrictions on transitive roles. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1719-1725. ijcai.org, 2019. URL: https://doi.org/10.24963/ijcai.2019/238.
  13. Víctor Gutiérrez-Basulto, Yazmín Angélica Ibáñez-García, and Jean Christoph Jung. Number restrictions on transitive roles in description logics with nominals. In Satinder Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA, pages 1121-1127. AAAI Press, 2017. URL: http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14357.
  14. Víctor Gutiérrez-Basulto, Yazmín Angélica Ibáñez-García, and Jean Christoph Jung. Answering regular path queries over SQ ontologies. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 1845-1852. AAAI Press, 2018. URL: https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16242.
  15. Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for very expressive description logics. Logic Journal of the IGPL, 8(3):239-263, 2000. URL: https://doi.org/10.1093/jigpal/8.3.239.
  16. Mark Kaminski and Gert Smolka. Terminating tableaux for SOQ with number restrictions on transitive roles. In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 213-228. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15240-5_16.
  17. Yevgeny Kazakov and Ian Pratt-Hartmann. A note on the complexity of the satisfiability problem for graded modal logics. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 407-416. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.17.
  18. Yevgeny Kazakov, Ulrike Sattler, and Evgeny Zolin. How many legs do I have? Non-simple roles in number restrictions revisited. In Nachum Dershowitz and Andrei Voronkov, editors, Proc. of the 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2007), volume 4790 of Lecture Notes in Computer Science, pages 303-317. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75560-9_23.
  19. Emanuel Kieroński. Results on the guarded fragment with equivalence or transitive relations. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 309-324. Springer, 2005. URL: https://doi.org/10.1007/11538363_22.
  20. Emanuel Kieroński. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006. URL: https://doi.org/10.1016/j.ic.2006.08.001.
  21. Emanuel Kieroński. Decidability issues for two-variable logics with several linear orders. In Marc Bezem, editor, Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume 12 of LIPIcs, pages 337-351. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.CSL.2011.337.
  22. Emanuel Kieroński and Adam Malinowski. The triguarded fragment with transitivity. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 334-353. EasyChair, 2020. URL: https://doi.org/10.29007/z359.
  23. Emanuel Kieroński and Sebastian Rudolph. Finite model theory of the triguarded fragment and related logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470734.
  24. Emanuel Kieroński and Lidia Tendera. Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants. ACM Trans. Comput. Log., 19(2):8:1-8:34, 2018. URL: https://doi.org/10.1145/3174805.
  25. Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6(3):467-480, 1977. URL: https://doi.org/10.1137/0206033.
  26. Ian Pratt-Hartmann. The two-variable fragment with counting and equivalence. Mathematical Logic Quarterly, 61(6):474-515, 2015. URL: https://doi.org/10.1002/malq.201400102.
  27. Ian Pratt-Hartmann. Fluted logic with counting. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 141:1-141:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.141.
  28. Ian Pratt-Hartmann, Wiesław Szwast, and Lidia Tendera. Quine’s fluted fragment is non-elementary. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 39:1-39:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.39.
  29. Ian Pratt-Hartmann, Wiesław Szwast, and Lidia Tendera. The fluted fragment revisited. Journal of Symbolic Logic, 84(3):1020-1048, 2019. URL: https://doi.org/10.1017/jsl.2019.33.
  30. Ian Pratt-Hartmann and Lidia Tendera. The fluted fragment with transitive relations. Annals of Pure and Applied Logic, 173(1):103042, 2022. URL: https://doi.org/10.1016/j.apal.2021.103042.
  31. William C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 61(2):608-620, 1996. URL: https://doi.org/10.2307/2275678.
  32. William C. Purdy. Complexity and nicety of fluted logic. Studia Logica, 71:177-198, 2002. URL: https://doi.org/10.1023/A:1016596721799.
  33. Sebastian Rudolph. Undecidability results for database-inspired reasoning problems in very expressive description logics. In Chitta Baral, James P. Delgrande, and Frank Wolter, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016, pages 247-257. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12787.
  34. Wiesław Szwast and Lidia Tendera. The guarded fragment with transitive guards. Ann. Pure Appl. Log., 128(1-3):227-276, 2004. URL: https://doi.org/10.1016/j.apal.2004.01.003.
  35. Stephan Tobies. Complexity results and practical algorithms for logics in knowledge representation, 2001. PhD Thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany. Google Scholar
  36. Stephan Tobies. PSPACE reasoning for graded modal logics. J. of Logic and Computation, 11(1):85-106, 2001. URL: https://doi.org/10.1093/logcom/11.1.85.
  37. Evgeny Zolin. Undecidability of the transitive graded modal logic with converse. J. Log. Comput., 27(5):1399-1420, 2017. URL: https://doi.org/10.1093/logcom/exw026.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact