public final class Prove extends CommandBase
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
Name |
Constructor and Description |
---|
Prove(Identifier ident)
create a prove command
|
Modifier and Type | Method and Description |
---|---|
Identifier |
getIdent()
get name of formula to be proved
|
void |
printCore(java.io.PrintWriter out)
Prints text representation on out (without new line termination).
|
void |
process()
process command "prove f": start proof of formula denoted by identifier f.
|
static void |
prove(FormulaSymbol symbol)
Prove formula denoted by symbol.
|
getName, toCommand, toNode, toString
public static final java.lang.String Name
public Prove(Identifier ident)
ident
- name of goal formula to be provedpublic Identifier getIdent()
public void process()
public static void prove(FormulaSymbol symbol)
symbol
- the symbol of the formula to be proved.public void printCore(java.io.PrintWriter out)
printCore
in class CommandBase
out
- the stream on which the text is written