Pandora.Help
Class HelpMessages

java.lang.Object
  Pandora.Help.HelpMessages

public class HelpMessages
extends java.lang.Object

Class which keeps all the help messages.

Field Summary

static java.lang.String	and
java.lang.String	and_elimination
java.lang.String	and_elimination_input_left
java.lang.String	and_elimination_input_right
static java.lang.String	arrow
static java.lang.String	em
static java.lang.String	falsity
static java.lang.String	falsity_elimination_forwards
java.lang.String	forall_elimination_backwards_input
static java.lang.String	forall_elimination_backwards_optional
java.lang.String	forall_elimination_backwards_specify
java.lang.String	forall_elimination_backwards_specify_input
java.lang.String	forall_elimination_forwards
static java.lang.String	forall_introduction_forwards
static java.lang.String	foralltick_backwards
Formula	formula
static java.lang.String	iff
static java.lang.String	iff_introduction
static java.lang.String	implies_introduction_forwards
static java.lang.String	lemma_forwards_backwards
static java.lang.String	not
static java.lang.String	not_introduction
static java.lang.String	notElim_backwards
static java.lang.String	notnot
static java.lang.String	or
java.lang.String	or_elimination_forwards
static java.lang.String	or_introduction_backwards
static java.lang.String	or_introduction_forwards
java.lang.String	or_introduction_forwards_input_left
java.lang.String	or_introduction_forwards_input_right
static java.lang.String	pc
static java.lang.String	reflexivity_forwards
static java.lang.String	reflexivity_forwards_no_constants
NDRule	rule
static java.lang.String	subs_backwards
static java.lang.String	subs_forwards
static java.lang.String	thereexist_elimination_forwards
static java.lang.String	thereExists
java.lang.String	thereexists_introduction_backwards
java.lang.String	thereexists_introduction_backwards_no_constants
java.lang.String	thereexists_introduction_forwards_input
static java.lang.String	thereexists_introduction_forwards_optional
static java.lang.String	thereexists_introduction_forwards_specify
static java.lang.String	thereexists_introduction_forwards_specify_input
static java.lang.String	tm
static java.lang.String	tm_backwards
static java.lang.String	tm_forwards
static java.lang.String	tm_tick
static java.lang.String	tm_tick_backwards
static java.lang.String	truth

Constructor Summary

HelpMessages(Formula formula)

HelpMessages(NDRule rule)

Method Summary

java.lang.String	displayFormula()
java.lang.String	displayFormula(Formula formula)
Formula	getFormula(NDRule rule)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

rule

public NDRule rule

formula

public Formula formula

and_elimination

public java.lang.String and_elimination

and_elimination_input_right

public java.lang.String and_elimination_input_right

and_elimination_input_left

public java.lang.String and_elimination_input_left

or_elimination_forwards

public java.lang.String or_elimination_forwards

or_introduction_forwards_input_right

public java.lang.String or_introduction_forwards_input_right

or_introduction_forwards_input_left

public java.lang.String or_introduction_forwards_input_left

thereexists_introduction_backwards

public java.lang.String thereexists_introduction_backwards

thereexists_introduction_backwards_no_constants

public java.lang.String thereexists_introduction_backwards_no_constants

thereexists_introduction_forwards_input

public java.lang.String thereexists_introduction_forwards_input

forall_elimination_backwards_input

public java.lang.String forall_elimination_backwards_input

forall_elimination_backwards_specify

public java.lang.String forall_elimination_backwards_specify

forall_elimination_backwards_specify_input

public java.lang.String forall_elimination_backwards_specify_input

forall_elimination_forwards

public java.lang.String forall_elimination_forwards

tm

public static final java.lang.String tm

See Also:

Constant Field Values

tm_backwards

public static final java.lang.String tm_backwards

See Also:

Constant Field Values

tm_forwards

public static final java.lang.String tm_forwards

See Also:

Constant Field Values

tm_tick

public static final java.lang.String tm_tick

See Also:

Constant Field Values

tm_tick_backwards

public static final java.lang.String tm_tick_backwards

See Also:

Constant Field Values

or_introduction_backwards

public static final java.lang.String or_introduction_backwards

See Also:

Constant Field Values

or_introduction_forwards

public static final java.lang.String or_introduction_forwards

See Also:

Constant Field Values

implies_introduction_forwards

public static final java.lang.String implies_introduction_forwards

See Also:

Constant Field Values

not_introduction

public static final java.lang.String not_introduction

See Also:

Constant Field Values

falsity_elimination_forwards

public static final java.lang.String falsity_elimination_forwards

See Also:

Constant Field Values

iff_introduction

public static final java.lang.String iff_introduction

See Also:

Constant Field Values

pc

public static final java.lang.String pc

See Also:

Constant Field Values

em

public static final java.lang.String em

See Also:

Constant Field Values

reflexivity_forwards

public static final java.lang.String reflexivity_forwards

See Also:

Constant Field Values

reflexivity_forwards_no_constants

public static final java.lang.String reflexivity_forwards_no_constants

See Also:

Constant Field Values

lemma_forwards_backwards

public static final java.lang.String lemma_forwards_backwards

See Also:

Constant Field Values

forall_introduction_forwards

public static final java.lang.String forall_introduction_forwards

See Also:

Constant Field Values

thereexists_introduction_forwards_optional

public static final java.lang.String thereexists_introduction_forwards_optional

See Also:

Constant Field Values

thereexists_introduction_forwards_specify

public static final java.lang.String thereexists_introduction_forwards_specify

See Also:

Constant Field Values

thereexists_introduction_forwards_specify_input

public static final java.lang.String thereexists_introduction_forwards_specify_input

See Also:

Constant Field Values

thereexist_elimination_forwards

public static final java.lang.String thereexist_elimination_forwards

See Also:

Constant Field Values

forall_elimination_backwards_optional

public static final java.lang.String forall_elimination_backwards_optional

See Also:

Constant Field Values

and

public static final java.lang.String and

See Also:

Constant Field Values

or

public static final java.lang.String or

See Also:

Constant Field Values

arrow

public static final java.lang.String arrow

See Also:

Constant Field Values

iff

public static final java.lang.String iff

See Also:

Constant Field Values

falsity

public static final java.lang.String falsity

See Also:

Constant Field Values

truth

public static final java.lang.String truth

See Also:

Constant Field Values

not

public static final java.lang.String not

See Also:

Constant Field Values

notElim_backwards

public static final java.lang.String notElim_backwards

See Also:

Constant Field Values

notnot

public static final java.lang.String notnot

See Also:

Constant Field Values

thereExists

public static final java.lang.String thereExists

See Also:

Constant Field Values

subs_forwards

public static final java.lang.String subs_forwards

See Also:

Constant Field Values

subs_backwards

public static final java.lang.String subs_backwards

See Also:

Constant Field Values

foralltick_backwards

public static final java.lang.String foralltick_backwards

See Also:

Constant Field Values

Constructor Detail

HelpMessages

public HelpMessages(NDRule rule)

HelpMessages

public HelpMessages(Formula formula)

Method Detail

displayFormula

public java.lang.String displayFormula()

displayFormula

public java.lang.String displayFormula(Formula formula)

getFormula

public Formula getFormula(NDRule rule)