Interface | Description |
---|---|
Answer |
Interface to prover answers.
|
ProofStateListener |
Listener that is notified if proof state has changed.
|
Prover |
Class | Description |
---|---|
AnswerBase |
Base class of prover answers.
|
Formula |
A formula occuring in a proof state.
|
GroundExpressions |
Compute ground (sub)expressions.
|
Instantiating |
Extending a proof state by instantiating quantified formulas.
|
InvalidAnswer |
Answer that formula is invalid.
|
Proof |
A proof represented by a tree of proof states.
|
ProofState |
The state of a proof.
|
ProofUtil |
Proving utilities.
|
ProverReasoning |
Reasoning with the help of an external prover.
|
Rewriting |
A visitor for rewriting expressions to a more human-friendly form.
|
Substitute |
Substitute in an expression all free occurences of denoted variables.
|
UnknownAnswer |
Answer that truth of formula is unknown.
|
ValidAnswer |
Answer that formula is valid.
|