fmrisc.ProofNavigator.Commands
Class Prove

java.lang.Object
  fmrisc.ProofNavigator.Commands.CommandBase
      fmrisc.ProofNavigator.Commands.Prove

All Implemented Interfaces:

Command

public final class Prove
extends CommandBase

"prove": prove goal formula.

Field Summary

static java.lang.String

Name

Constructor Summary

Prove(Identifier ident)
create a prove command

Method Summary

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.

Methods inherited from class fmrisc.ProofNavigator.Commands.CommandBase

getName, toCommand, toNode, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

Name

public static final java.lang.String Name

See Also:

Constant Field Values

Constructor Detail

Prove

public Prove(Identifier ident)

create a prove command

Parameters:

ident - name of goal formula to be proved

Method Detail

getIdent

public Identifier getIdent()

get name of formula to be proved

Returns:

name of formula to be proved

process

public void process()

process command "prove f": start proof of formula denoted by identifier f.

printCore

public void printCore(java.io.PrintWriter out)

Prints text representation on out (without new line termination).

Specified by:

printCore in class CommandBase

Parameters:

out - the stream on which the text is written