Formal proofs about rewriting using ACL2

DOI10.1023/A:1016003314081zbMath1015.68169MaRDI QIDQ1610218

Jose Antonio Alonso, Francisco Jesús Martín-Mateos, José Luis Ruiz-Reina, María José Hidalgo

Publication date: 19 August 2002

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

theorem provingformal verificationrewritingrewrite systemsACL2

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Unnamed Item, Formal correctness of a quadratic unification algorithm, A formalization of the Knuth-Bendix(-Huet) critical pair theorem, A PVS Theory for Term Rewriting Systems, A verified common lisp implementation of Buchberger's algorithm in ACL2

Uses Software

• ACL2
• LISP
• Ivy