Rewriting with equivalence relations in ACL2

DOI10.1007/s10817-007-9095-9zbMath1140.68029OpenAlexW1966353549MaRDI QIDQ928668

Matt Kaufmann, J. Strother Moore

Publication date: 11 June 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-007-9095-9

zbMATH Keywords

RefinementCongruenceEquivalence relationsRewriting

Mathematics Subject Classification ID

Related Items (3)

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ A formalization of powerlist algebra in ACL2 ⋮ Limited second-order functionality in a first-order setting

Uses Software

• ACL2
• Isabelle/HOL
• NQTHM

Cites Work

• Structured theory development for a mechanized logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Special relations in automated deduction
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Rewriting with equivalence relations in ACL2