LIPIcs.FSCD.2017.19.pdf
- Filesize: 0.58 MB
- 16 pages
Document
Infinite Runs in Abstract Completion
Authors
-
Part of:
Volume:
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-30
Cite AsGet BibTex
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. Infinite Runs in Abstract Completion. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.19
https://doi.org/10.4230/LIPIcs.FSCD.2017.19
Abstract
Completion is one of the first and most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In an earlier paper we presented a new and formalized correctness proof of abstract completion for finite runs. In this paper we extend our analysis and our formalization to infinite runs, resulting in a new proof that fair infinite runs produce complete presentations of the initial equations. We further consider ordered completion - an important extension of completion that aims to produce ground-complete presentations of the initial equations. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
Keywords
- term rewriting
- abstract completion
- ordered completion
- canonicity
- Isabelle/HOL
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
-
L. Bachmair. Canonical Equational Proofs. Birkhäuser, 1991.
- L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In Proc. 8th International Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, pages 5-20, 1986. URL: http://dx.doi.org/10.1007/3-540-16780-3_76.
-
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symposium on Logic in Computer Science, pages 346-357, 1986.
-
L. Bachmair, N. Dershowitz, and D. A. Plaisted. Completion without failure. In H. Aït Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2: Rewriting Techniques of Progress in Theoretical Computer Science, pages 1-30. Academic Press, 1989.
- S. Burckel. Syntactical methods for braids of three strands. Journal of Symbolic Computation, 31:557-564, 2001. URL: http://dx.doi.org/10.1006/jsco.2000.0473.
- B. Gramlich. On interreduction of semi-complete term rewriting systems. Theoretical Computer Science, 258(1-2):435-451, 2001. URL: http://dx.doi.org/10.1016/S0304-3975(00)00030-X.
- N. Hirokawa, A. Middeldorp, and C. Sternagel. A new and formalized proof of abstract completion. In Proc. 5th International Conference on Interactive Theorem Proving, volume 8558 of Lecture Notes in Computer Science, pages 292-307, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_19.
-
S. Kamin and J. J. Lévy. Two generalizations of the recursive path ordering. Unpublished manuscript, University of Illinois, 1980.
- D. Kapur and P. Narendran. A finite Thue system with decidable word problem and without equivalent finite canonical system. Theoretical Computer Science, 35:337-344, 1985. URL: http://dx.doi.org/10.1016/0304-3975(85)90023-4.
-
J. W. Klop. Combinatory Reduction Systems. PhD thesis, Utrecht University, 1980.
-
D. E. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. 1970.
- Y. Métivier. About the rewriting systems produced by the Knuth-Bendix completion algorithm. Information Processing Letters, 16(1):31-34, 1983. URL: http://dx.doi.org/10.1016/0020-0190(83)90009-1.
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45949-9.
- C. Sternagel and R. Thiemann. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of Leibniz International Proceedings in Informatics, pages 287-302. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. doi: 10.4230/LIPIcs.RTA.2013.287. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2013.287.
-
Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
- V. van Oostrom. Confluence by decreasing diagrams - converted. In Proc. 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 306-320, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70590-1_21.
-
F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In Proc. Colloquium on Algebra, Combinatorics and Logic in Computer Science, Vol. II, volume 42 of Colloquia Mathematica Societatis J. Bolyai, pages 849-869, 1986.