Package | Description |
---|---|
fmrisc.ProofNavigator.Commands | |
fmrisc.ProofNavigator.Communication | |
fmrisc.ProofNavigator.Proving | |
fmrisc.ProofNavigator.Semantics | |
fmrisc.ProofNavigator.Syntax |
Modifier and Type | Method and Description |
---|---|
FormulaSymbol[] |
Lemma.getSymbols(Environment env)
Return symbols of formulas referenced in lemma.
|
Modifier and Type | Method and Description |
---|---|
static void |
Prove.prove(FormulaSymbol symbol)
Prove formula denoted by symbol.
|
Modifier and Type | Method and Description |
---|---|
boolean |
Store.existsProof(FormulaSymbol symbol)
Check whether store holds proof of formula.
|
Proof |
Store.readProof(FormulaSymbol symbol)
Read proof for formula from store.
|
Modifier and Type | Method and Description |
---|---|
FormulaSymbol |
Proof.getSymbol()
get symbol of formula proved
|
Modifier and Type | Method and Description |
---|---|
static Proof |
Proof.newProof(FormulaSymbol symbol,
boolean autoSimplify,
State.ProverVersion proverVersion,
boolean firstOrder,
boolean toLogical)
Construct new proof for formula denoted by symbol.
|
static Proof |
Proof.toProof(FormulaSymbol symbol,
org.w3c.dom.Node node)
Construct skeleton proof from DOM representation.
|
Modifier and Type | Method and Description |
---|---|
FormulaSymbol |
Environment.getFormulaSymbol(Identifier name)
returns symbol associated to name (null, if none)
|
FormulaSymbol |
FormulaTable.getSymbol(Identifier name)
returns symbol associated to name (null, if none)
|
FormulaSymbol |
FormulaTable.put(FormulaDeclIdentifier key,
Expression formula,
boolean axiom,
Environment env)
put formula in formula table
|
FormulaSymbol |
Environment.putFormula(FormulaDeclIdentifier name,
Expression formula,
boolean axiom)
put formula in environment
|
FormulaSymbol |
Environment.putFormulaDeclaration(FormulaDeclaration fdecl)
put formula declaration into environment
|
Modifier and Type | Method and Description |
---|---|
void |
Environment.putFormulaSymbol(FormulaSymbol symbol)
add formula symbol to environment
|
Modifier and Type | Method and Description |
---|---|
FormulaSymbol |
FormulaDeclIdentifier.getSymbol()
returns formula symbol
|