Document Open Access Logo

On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems

Authors Franz Baader , Jürgen Giesl

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.16.pdf
  • Filesize: 0.71 MB
  • 18 pages

Document Identifiers

Author Details

Franz Baader
  • Theoretical Computer Science, TU Dresden, Germany
  • SCADS.AI Dresden/Leipzig, Germany
Jürgen Giesl
  • RWTH Aachen University, Aachen, Germany

Funding

  • Baader, Franz: Partially supported by DFG, Grant 389792660, within TRR 248 "Center for Perspicuous Computing", and by the German Federal Ministry of Education and Research (BMBF, SCADS22B) and the Saxon State Ministry for Science, Culture and Tourism (SMWK) by funding the competence center for Big Data and AI "ScaDS.AI Dresden/Leipzig".
  • Giesl, Jürgen: Partially supported by DFG, Grant 235950644 (Project GI 274/6-2).

Cite AsGet BibTex

Franz Baader and Jürgen Giesl. On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.16

Abstract

Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system R, a term s, and a natural number n, decide whether there is a term t of size ≤ n reachable from s using the rules of R. We investigate the complexity of this problem depending on how termination of R can be established. We show that the problem is NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Automated reasoning
  • Theory of computation → Complexity theory and logic
Keywords
  • Rewriting
  • Termination
  • Confluence
  • Creating small terms
  • Derivational complexity
  • Description Logics
  • Proof rewriting

Metrics

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

References

  1. Beatriz Alarcón, Salvador Lucas, and José Meseguer. A dependency pair framework for A∨ C-termination. In Peter Csaba Ölveczky, editor, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Revised Selected Papers, volume 6381 of Lecture Notes in Computer Science, pages 35-51. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16310-4_4.
  2. Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann, and Julián Méndez. Evonne: Interactive proof visualization for description logics (system description). In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 271-280. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_16.
  3. Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova. Finding small proofs for description logic entailments: Theory and practice. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Proceedings, volume 73 of EPiC Series in Computing, pages 32-67. EasyChair, 2020. URL: https://doi.org/10.29007/NHPP.
  4. Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova. Finding good proofs for description logic entailments using recursive quality measures. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 291-308. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_17.
  5. Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pages 364-369. Professional Book Center, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0372.pdf.
  6. Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. Google Scholar
  7. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  8. Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. Theor. Comput. Sci., 67(2&3):173-201, 1989. URL: https://doi.org/10.1016/0304-3975(89)90003-0.
  9. Guillaume Bonfante, Adam Cichon, Jean-Yves Marion, and Hélène Touzet. Algorithms with polynomial interpretation termination proof. J. Funct. Program., 11(1):33-53, 2001. URL: https://doi.org/10.1017/S0956796800003877.
  10. Guillaume Bonfante and Georg Moser. Characterising space complexity classes via Knuth-Bendix orders. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 142-156. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16242-8_11.
  11. Jürgen Giesl and Deepak Kapur. Dependency pairs for equational rewriting. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Proceedings, volume 2051 of Lecture Notes in Computer Science, pages 93-108. Springer, 2001. URL: https://doi.org/10.1007/3-540-45127-7_9.
  12. Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann. Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst., 33(2):7:1-7:39, 2011. URL: https://doi.org/10.1145/1890028.1890030.
  13. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. J. Autom. Reason., 37(3):155-203, 2006. URL: https://doi.org/10.1007/S10817-006-9057-7.
  14. Dieter Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci., 105(1):129-140, 1992. URL: https://doi.org/10.1016/0304-3975(92)90289-R.
  15. Dieter Hofbauer. An upper bound on the derivational complexity of Knuth-Bendix orderings. Inf. Comput., 183(1):43-56, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00008-7.
  16. Dieter Hofbauer and Clemens Lautemann. Termination proofs and the length of derivations (preliminary version). In Nachum Dershowitz, editor, Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Proceedings, volume 355 of Lecture Notes in Computer Science, pages 167-177. Springer, 1989. URL: https://doi.org/10.1007/3-540-51081-8_107.
  17. Gérard Huet and Dallas S. Lankford. On the uniform halting problem for term rewriting systems. INRIA Rapport de Recherche No. 283, 1978. URL: https://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Huet_Lankford.pdf.
  18. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Comput., 15(4):1155-1194, 1986. URL: https://doi.org/10.1137/0215084.
  19. Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theor. Comput. Sci., 104(1):29-51, 1992. URL: https://doi.org/10.1016/0304-3975(92)90165-C.
  20. Yevgeny Kazakov, Markus Krötzsch, and Frantisek Simancik. The incredible ELK - from polynomial procedures to efficient reasoning with EL ontologies. J. Autom. Reason., 53(1):1-61, 2014. URL: https://doi.org/10.1007/S10817-013-9296-3.
  21. Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra. Pergamon Press, Oxford, 1970. Google Scholar
  22. Dallas S. Lankford. On proving term rewriting systems are Noetherian. Memo MTP-3, Math. Dept., Louisiana Technical University, Ruston, LA, 1979. URL: http://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Lankford_Poly_Term.pdf.
  23. Ingo Lepper. Derivation lengths and order types of Knuth-Bendix orders. Theor. Comput. Sci., 269(1-2):433-450, 2001. URL: https://doi.org/10.1016/S0304-3975(01)00015-9.
  24. Ingo Lepper. Simply terminating rewrite systems with long derivations. Arch. Math. Log., 43(1):1-18, 2004. URL: https://doi.org/10.1007/S00153-003-0190-2.
  25. Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, Vol. I, pages 371-443. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50009-6.
  26. Albert Rubio. A fully syntactic AC-RPO. Inf. Comput., 178(2):515-533, 2002. URL: https://doi.org/10.1006/INCO.2002.3158.
  27. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2):177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
  28. TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  29. Andreas Weiermann. Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. Theor. Comput. Sci., 139(1&2):355-362, 1995. URL: https://doi.org/10.1016/0304-3975(94)00135-6.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact