Tools, utilities, and strategies for dealing with particular kinds
- A symbolic simulation framework for proving finitely bounded ACL2
theorems by bit-blasting with a Binary Decision
Diagram (BDD) package or a SAT
- Clause processor for quantifier-based reasoning.
- A powerful automated termination prover for ACL2
- Install an unnormalized definition
- Rewrite a term
- Compute runes to disable
- A prover framework that supports bit-blasting.
- Efficiency considerations
- Substitute upper bounds and lower bounds for subterms in comparisons.
- Bash is a tool that simplifies a term, producing a list of
simplified terms such that if all output terms are theorems, then so is the
- Generic framework that allows simple traversals of DAGs.
- Ordered binary decision diagrams with rewriting
- Macro for defining a theorem with a minimal set of hypotheses
- A meta-rule system that lets the ACL2 rewriter pass around contextual
information. Similar to Dave Greve's NARY. This extends ACL2's notion of
- Simp returns a list of simplified versions of its input
term, each paired with a hypothesis list under which the input and output
terms are provably equal.
- Rewrite a list of hypotheses
- Bash-term-to-dnf is a tool that simplifies a term, producing
a list of clauses such that if all output clauses are theorems, then so is the
- Override ACL2's built-in ancestors check heuristic with a simpler and less surprising one.
- Compute runes to leave enabled
- Noteworthy clause-processors
- Prove that a function called on its formals equals its body
- Perform proofs without subsumption/replacement to preserve hypotheses that might otherwise be dropped.
- A hint to induce ACL2 to perform substitutions using equivalence relations from the hypothesis
- Find and prove upper and lower bounds for an expression, following a series of simplification steps.
- Rewrite a list of contextual assumptions
- Find true conclusions using GL
- Tools that produce hints to guide the prover.