Proof-automation
Tools, utilities, and strategies for dealing with particular kinds
of proofs.
Subtopics
- Gl
- A symbolic simulation framework for proving finitely bounded ACL2
theorems by bit-blasting with a Binary Decision
Diagram (BDD) package or a SAT
solver.
- Witness-cp
- Clause processor for quantifier-based reasoning.
- Ccg
- A powerful automated termination prover for ACL2
- Install-not-normalized
- Install an unnormalized definition
- Rewrite$
- Rewrite a term
- Removable-runes
- Compute runes to disable
- Fgl
- A prover framework that supports bit-blasting.
- Efficiency
- Efficiency considerations
- Rewrite-bounds
- Substitute upper bounds and lower bounds for subterms in comparisons.
- Bash
- 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
input term.
- Def-dag-measure
- Generic framework that allows simple traversals of DAGs.
- Bdd
- Ordered binary decision diagrams with rewriting
- Remove-hyps
- Macro for defining a theorem with a minimal set of hypotheses
- Contextual-rewriting
- 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
congruence-based rewriting.
- Simp
- 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$-hyps
- Rewrite a list of hypotheses
- Bash-term-to-dnf
- 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
input term.
- Use-trivial-ancestors-check
- Override ACL2's built-in ancestors check heuristic with a simpler and less surprising one.
- Minimal-runes
- Compute runes to leave enabled
- Clause-processor-tools
- Noteworthy clause-processors
- Fn-is-body
- Prove that a function called on its formals equals its body
- Without-subsumption
- Perform proofs without subsumption/replacement to preserve hypotheses that might otherwise be dropped.
- Rewrite-equiv-hint
- A hint to induce ACL2 to perform substitutions using equivalence relations from the hypothesis
- Def-bounds
- Find and prove upper and lower bounds for an expression, following a series of simplification steps.
- Rewrite$-context
- Rewrite a list of contextual assumptions
- Try-gl-concls
- Find true conclusions using GL
- Hint-utils
- Tools that produce hints to guide the prover.
