Package | Description |
---|---|
fmrisc.ProofNavigator.Proving |
Modifier and Type | Method and Description |
---|---|
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<Formula> v)
converts vector v of Formula objects to array
|
static Formula[] |
ProofUtil.toFormulaArray(java.util.Vector<Formula> v)
converts vector v of Formula objects to Formula array
|
Modifier and Type | Method and Description |
---|---|
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.
|
Modifier and Type | Method and Description |
---|---|
static Formula[] |
Formula.toArray(java.util.Vector<Formula> v)
converts vector v of Formula objects to array
|
static Formula[] |
ProofUtil.toFormulaArray(java.util.Vector<Formula> v)
converts vector v of Formula objects to Formula array
|
Constructor and Description |
---|
Formula(ProofState state,
Formula formula)
construct a copy of the given formula in the denoted state
|