Formal proofs about rewriting using ACL2
From MaRDI portal
Publication:1610218
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)
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