LIPIcs.ITP.2023.38.pdf
- Filesize: 0.69 MB
- 8 pages
Document
Formalizing Almost Development Closed Critical Pairs (Short Paper)
Authors
Christina Kohl 
,
Aart Middeldorp
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Cite As Get 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)
0PDF Downloads
References
- Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
- 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.
- 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.
- 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.
- 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.
- 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.
-
TeReSe, editor. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
-
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.
- 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.
- Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00173-9.