Formal proofs about rewriting using ACL2
From MaRDI portal
Recommendations
- Formalizing rewriting in the ACL2 theorem prover
- Rewriting with equivalence relations in ACL2
- A formal proof of Dickson's lemma in ACL2
- Certifying proofs in the first-order theory of rewriting
- Verification in ACL2 of a generic framework to synthesize SAT-provers
- Proof-pattern recognition and lemma discovery in ACL2
- Structural Proof Theory as Rewriting
- Toward a verification logic for rewriting logic
- Proving Safety Properties of Rewrite Theories
Cited in
(18)- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Rough diamond: an extension of equivalence-based rewriting
- Certifying confluence proofs via relative termination and rule labeling
- A formalization of Newman's and Yokouchi's lemmas in a higher-order language
- Formalizing rewriting in the ACL2 theorem prover
- scientific article; zbMATH DE number 2154398 (Why is no real title available?)
- Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
- A PVS theory for term rewriting systems
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Meta Reasoning in ACL2
- Logic Based Program Synthesis and Transformation
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- A higher-order implementation of rewriting
- Abstract abstract reduction
- Formal correctness of a quadratic unification algorithm
- Term rewriting and beyond -- theorem proving in Isabelle
- Rewriting with equivalence relations in ACL2
This page was built for publication: Formal proofs about rewriting using ACL2
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1610218)
