Uses of Class
fmrisc.Proving.Formula

Packages that use Formula

fmrisc.Proving

Uses of Formula in fmrisc.Proving

Methods in fmrisc.Proving that return Formula

Formula[]	ProofState.add(Formula[] formulas, Formula formula) Adds a formula to a sequence of formulas in this state.
Formula[]	ProofState.add(Formula[] formulas, Formula[] formulas0) Adds a sequence of formulas to a sequence of formulas in this state.
Formula[]	ProofState.copy(Formula[] formulas) Copy a sequence of formulas in this state.
Formula	ProofState.getAssumption(java.lang.String label) returns assumption with denoted label
Formula[]	ProofState.getAssumptions() get assumptions of proof state
Formula[]	ProofState.getAxioms() get axioms of proof state
Formula	ProofState.getFormula(java.lang.String label) returns formula (assumption or goal) with denoted label
Formula	ProofState.getGoal(java.lang.String label) returns goal with denoted label
Formula[]	ProofState.getGoals() get goals of proof state
Formula[]	ProofState.remove(Formula[] formulas, Formula formula) Remove a formula from a sequence of formulas in this state.
Formula[]	ProofState.replace(Formula[] formulas, Formula formula, Formula rformula) Replace a formula in a sequence of formulas in this state.
static Formula[]	Formula.toArray(java.util.Vector v) converts vector v of Formula objects to array
static Formula[]	ProofUtil.toFormulaArray(java.util.Vector v) converts vector v of Formula objects to Formula array

Methods in fmrisc.Proving with parameters of type Formula

Formula[]	ProofState.add(Formula[] formulas, Formula formula) Adds a formula to a sequence of formulas in this state.
Formula[]	ProofState.add(Formula[] formulas, Formula formula) Adds a formula to a sequence of formulas in this state.
Formula[]	ProofState.add(Formula[] formulas, Formula[] formulas0) Adds a sequence of formulas to a sequence of formulas in this state.
Formula[]	ProofState.add(Formula[] formulas, Formula[] formulas0) Adds a sequence of formulas to a sequence of formulas in this state.
Formula[]	ProofState.copy(Formula[] formulas) Copy a sequence of formulas in this state.
static ProofState	Instantiating.instantiate(Formula formula) Extend proof state by instantiations of given formula
static ProofState	Instantiating.instantiate(Formula[] formulas) Extend proof state by instantiations of given formulas
Formula[]	ProofState.remove(Formula[] formulas, Formula formula) Remove a formula from a sequence of formulas in this state.
Formula[]	ProofState.remove(Formula[] formulas, Formula formula) Remove a formula from a sequence of formulas in this state.
Formula[]	ProofState.replace(Formula[] formulas, Formula formula, Formula rformula) Replace a formula in a sequence of formulas in this state.
Formula[]	ProofState.replace(Formula[] formulas, Formula formula, Formula rformula) Replace a formula in a sequence of formulas in this state.
void	ProofState.setAssumptions(Formula[] formulas) set assumptions of proof state
void	ProofState.setAxioms(Formula[] formulas) Set axioms of proof state.
void	ProofState.setGoals(Formula[] formulas) set goals of proof state
static boolean	ProverReasoning.simplify(ProofState state, Formula formula, boolean hard) Simplify a single formula in some proof state.

Constructors in fmrisc.Proving with parameters of type Formula

Formula(ProofState state, Formula formula)
construct a copy of the given formula in the denoted state