Package fmrisc.Proving

Interface Summary

Answer	Interface to prover answers.
ProofStateListener
Prover

Class Summary

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
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.