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