Abstract
Completion is one of the most studied techniques in term rewriting. We present a new proof of the correctness of abstract completion that is based on peak decreasingness, a special case of decreasing diagrams. Peak decreasingness replaces Newman’s Lemma and allows us to avoid proof orders in the correctness proof of completion. As a result, our proof is simpler than the one presented in textbooks, which is confirmed by our Isabelle/HOL formalization. Furthermore, we show that critical pair criteria are easily incorporated in our setting.
Supported by JSPS KAKENHI Grant Number 25730004 and the Austrian Science Fund (FWF) projects I963 and J3202.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)
Bachmair, L.: Canonical Equational Proofs. Birkhäuser (1991)
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the ACM 41(2), 236–276 (1994), doi:10.1145/174652.174655
Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs. In: Proc. 1st IEEE Symposium on Logic in Computer Science, pp. 346–357 (1986)
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Resolution of Equations in Algebraic Structures: Completion without Failure, vol. 2, pp. 1–30. Academic Press (1989)
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/ HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011), doi:10.1007/978-3-642-24364-6
Galdino, A.L., Ayala-Rincón, M.: A formalization of the Knuth-Bendix(-Huet) critical pair theorem. Journal of Automated Reasoning 45(3), 301–325 (2010), doi:10.1007/s10817-010-9165-2
Huet, G.: A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences 23(1), 11–21 (1981), doi:10.1016/0022-0000(81)90002-7
Huffman, B., Urban, C.: A new foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 35–50. Springer, Heidelberg (2010), doi:10.1007/978-3-642-14052-5_5
Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered in the Knuth-Bendix completion procedure. Journal of Symbolic Computation 6(1), 19–36 (1988), doi:10.1016/S0747-7171(88)80019-1
Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297 (1970)
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002), doi:10.1007/3-540-45949-9
van Oostrom, V.: Confluence by decreasing diagrams. Theoretical Computer Science 126(2), 259–280 (1994), doi:10.1016/0304-3975(92)00023-K
van Raamsdonk, F. (ed.): Proc. 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.-J., Martín-Mateos, F.-J.: Formal proofs about rewriting using ACL2. Annals of Mathematics and Artificial Intelligence 36(3), 239–262 (2002), doi:10.1023/A:1016003314081
Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: van Raamsdonk [14], pp. 287–302, doi:10.4230/LIPIcs.RTA.2013.287
Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in Nominal Isabelle. Logical Methods in Computer Science 8(2), 465–476 (2012), doi:10.2168/LMCS-8(2:14)2012
Winkler, F., Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Proc. Colloquium on Algebra, Combinatorics and Logic in Computer Science. Colloquia Mathematica Societatis J. Bolyai, vol. II, 42, pp. 849–869 (1986)
Zankl, H.: Decreasing diagrams – formalized. In: van Raamsdonk [14], pp. 352–367, doi:10.4230/LIPIcs.RTA.2013352
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Hirokawa, N., Middeldorp, A., Sternagel, C. (2014). A New and Formalized Proof of Abstract Completion. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-08970-6_19
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08969-0
Online ISBN: 978-3-319-08970-6
eBook Packages: Computer ScienceComputer Science (R0)