Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Community
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
X86isa
Axe
Axe-r1cs
Axe-lifters
Axe-core
Axe-provers
Prove-equal-with-axe
Prover-basic
Make-prover-simple
Defthm-stp
Defthm-axe-basic
Prover-legacy
Axe-rewriters
Axe-jvm
Axe-x86
Execloader
Math
Testing-utilities
Axe
Axe-provers
The Axe prover tools.
Subtopics
Prove-equal-with-axe
A tool for proving that DAGs / terms are equivalent.
Prover-basic
A basic, modern Axe prover.
Make-prover-simple
A tool to create custom Axe prover.
Defthm-stp
A defthm-like tool that uses the STP solver.
Defthm-axe-basic
A defthm-like tool that uses Axe.
Prover-legacy
The legacy Axe prover.