Formalizing Almost Development Closed Critical Pairs (Short Paper)

Authors Christina Kohl , Aart Middeldorp



PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.38.pdf
  • Filesize: 0.69 MB
  • 8 pages

Document Identifiers

Author Details

Christina Kohl
  • Universität Innsbruck, Austria
Aart Middeldorp
  • Universität Innsbruck, Austria

Cite AsGet BibTex

Christina Kohl and Aart Middeldorp. Formalizing Almost Development Closed Critical Pairs (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.38

Abstract

We report on the first formalization of the almost-development closedness criterion for confluence of left-linear term rewrite systems and illustrate a problem we encountered while trying to formalize the original paper proof by van Oostrom.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Logic and verification
Keywords
  • Term rewriting
  • confluence
  • certification

Metrics

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

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  2. Christina Kohl and Aart Middeldorp. ProTeM: A proof term manipulator (system description). In Hélène Kirchner, editor, Proc. 3rd International Conference on Formal Structures for Computation and Deduction, volume 108 of Leibniz International Proceedings in Informatics, pages 31:1-31:8, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.31.
  3. Christina Kohl and Aart Middeldorp. A formalization of the development closedness criterion for left-linear term rewrite systems. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic, editors, Proc. 12th International Conference on Certified Programs and Proofs, pages 197-210, 2023. URL: https://doi.org/10.1145/3573105.3575667.
  4. Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. CSI: New evidence - a progress report. In Leonardo de Moura, editor, Proc. 26th International Conference on Automated Deduction, volume 10395 of Lecture Notes in Artificial Intelligence, pages 385-397, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_24.
  5. Julian Nagele and René Thiemann. Certification of confluence proofs using CeTA. In Takahito Aoto and Delia Kesner, editors, Proc. 3rd International Workshop on Confluence, pages 19-23, 2014. Available from URL: http://cl-informatik.uibk.ac.at/iwc/iwc2014.pdf.
  6. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  7. TeReSe, editor. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  8. Yoshihito Toyama. Commutativity of term rewriting systems. In Kazuhiro Fuchi and Laurent Kott, editors, Programming of Future Generation Computers II, pages 393-407. North-Holland, 1988. Google Scholar
  9. Vincent van Oostrom. Development closed critical pairs. In Gilles Dowek, Jan Heering, Karl Meinke, and Bernhard Möller, editors, Proc. 2nd International Workshop on Higher-Order Algebra, Logic, and Term Rewriting, volume 1074 of Lecture Notes in Computer Science, pages 185-200, 1995. URL: https://doi.org/10.1007/3-540-61254-8_26.
  10. Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00173-9.
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