×

Formal proofs about rewriting using ACL2. (English) Zbl 1015.68169

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).

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems

Software:

ACL2; Ivy; LISP
PDFBibTeX XMLCite
Full Text: DOI