Ruiz-Reina, José-Luis; Alonso, José-Antonio; Hidalgo, María-José; Martín-Mateos, Francisco-Jesús Formal proofs about rewriting using ACL2. (English) Zbl 1015.68169 Ann. Math. Artif. Intell. 36, No. 3, 239-262 (2002). Summary: We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization and representation aspects of our work using the first-order, quantifier-free logic of ACL2 and we sketch some of the main points of the proof effort. First, we present a formalization of abstract reduction systems and then we show how this abstraction can be instantiated to establish results about term rewriting. The main theorems we mechanically proved are Newman’s lemma (for abstract reductions) and Knuth-Bendix critical pair theorem (for term rewriting). Cited in 5 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68Q42 Grammars and rewriting systems Keywords:theorem proving; ACL2; rewriting; formal verification; rewrite systems Software:ACL2; Ivy; LISP PDFBibTeX XMLCite \textit{J.-L. Ruiz-Reina} et al., Ann. Math. Artif. Intell. 36, No. 3, 239--262 (2002; Zbl 1015.68169) Full Text: DOI