| Pandora.Types |
public static final java.lang.String |
AndElim |
"\u2227E" |
public static final java.lang.String |
AndIntro |
"\u2227I" |
public static final java.lang.String |
Assume |
"ass" |
public static final java.lang.String |
EM |
"EM" |
public static final java.lang.String |
Empty |
"" |
public static final java.lang.String |
ExistsElim |
"\u2203E" |
public static final java.lang.String |
ExistsIntro |
"\u2203I" |
public static final java.lang.String |
FalsityElim |
"\u22a5E" |
public static final java.lang.String |
FalsityIntro |
"\u22a5I" |
public static final java.lang.String |
ForallArrowElim |
"\u2200\u2192E" |
public static final java.lang.String |
ForallArrowIntro |
"\u2200\u2192I" |
public static final java.lang.String |
ForallElim |
"\u2200E" |
public static final java.lang.String |
ForallIntro |
"\u2200I" |
public static final java.lang.String |
ForallTick |
"\u2200E\u221a" |
public static final java.lang.String |
Given |
"given" |
public static final java.lang.String |
Goal |
"<goal>" |
public static final java.lang.String |
IffElim |
"\u2194E" |
public static final java.lang.String |
IffIntro |
"\u2194I" |
public static final java.lang.String |
ImpliesElim |
"\u2192E" |
public static final java.lang.String |
ImpliesIntro |
"\u2192I" |
public static final java.lang.String |
Instantiate |
"inst" |
public static final java.lang.String |
LEMMA |
"Lemma" |
public static final java.lang.String |
NotElim |
"\u00acE" |
public static final java.lang.String |
NotIntro |
"\u00acI" |
public static final java.lang.String |
NotNot |
"\u00ac\u00ac" |
public static final java.lang.String |
OrElim |
"\u2228E" |
public static final java.lang.String |
OrIntro |
"\u2228I" |
public static final java.lang.String |
PC |
"PC" |
public static final java.lang.String |
Reflexivity |
"Reflexivity" |
public static final java.lang.String |
Skolem |
"\u2200Iconst" |
public static final java.lang.String |
Skolem2 |
"\u2203Econst" |
public static final java.lang.String |
Sub |
"=Sub" |
public static final java.lang.String |
Tick |
"\u221a" |
public static final java.lang.String |
TM |
"TM" |
public static final java.lang.String |
TMTick |
"TM\u221a" |
public static final java.lang.String |
TopIntro |
"\u22a4I" |
| Pandora.Help.HelpMessages |
public static final java.lang.String |
and |
"For example P \u2227 Q." |
public static final java.lang.String |
arrow |
"For example P \u2192 Q." |
public static final java.lang.String |
em |
"Input the formula you wish to apply the law on\n____________________________________\n\nHint: p results in p \u2228 \u00acp and \n \u00acp results in \u00acp \u2228 p \n\n" |
public static final java.lang.String |
falsity |
"For example \u22a5" |
public static final java.lang.String |
falsity_elimination_forwards |
"Input the formula you would like to introduce\n___________________________________\n\nHint: Since falsity implies anything you may\ninput whatever formula you want provided it is\nin the signature of your proof\n\n" |
public static final java.lang.String |
forall_elimination_backwards_optional |
"(Optionally) input the For All formula you\'d like to appear as the new goal\n_____________________________________________________________________________\n\nHint: if you have P(a,b) for example, you can deduce \u2200u(P(u,b)) or even\n\u2200u\u2200v(P(u,v)) for more help see the manual entry, for simple cases with\none variable click ok to skip to the next screen\n\n" |
public static final java.lang.String |
forall_introduction_forwards |
"Input the Formula you\'d like to be derived by For All Introduction Forwards\n___________________________________________________________________________\n\nHint: if you REALLY want to use this rule to derive \u2200x(P(x)) (the formula\nyou are asked to input in this screen) you will have to complete the proof\nfrom sk1 to P(sk1)\n\n" |
public static final java.lang.String |
foralltick_backwards |
"Lets look at an example which would succeed when for all elimination\ntick (backwards) is used, \u2200x\u2200y(p(x,f(y))) <derived line> \nand p(a,f(b)) <goal line>, but it would not succeed if the derived \nline is \u2200x(p(x,f(x))) since x can\'t be unified to both a and b." |
public static final java.lang.String |
iff |
"For example P \u2194 Q." |
public static final java.lang.String |
iff_introduction |
"Input the conclusion you would like to be derived by IFF Introduction Forwards\n_________________________________________________________________________________\n\nHint: If you want to use this rule to derive x \u2194 y (the formula you are asked\nto input in this screen) you will have to complete the proof from x to y\n\n" |
public static final java.lang.String |
implies_introduction_forwards |
"Input the conclusion you would like to be derived by Arrow Introduction Forwards\n__________________________________________________________________________________\n\nHint: If you want to use this rule to derive x \u2192 y (the formula you are asked\nto input in this screen) you will have to complete the proof from x to y.\n\n" |
public static final java.lang.String |
lemma_forwards_backwards |
"Enter the formula you would like to add as a lemma\n_______________________________________\n\nHint: A new goal (which you need to specify in this\nscreen) and an empty line will appear in the middle\nof your proof as a lemma which you need to prove\n\n" |
public static final java.lang.String |
not |
"For example P and \u00acP" |
public static final java.lang.String |
not_introduction |
"Input the conclusion you would like to be derived by Not Introduction Forwards\n________________________________________________________________________________\n\nHint: If you want to use this rule to derive \u00acx (the formula you are asked\nto input in this screen) you will have to complete the proof from x to \u22a5.\n\n" |
public static final java.lang.String |
notElim_backwards |
"A goal \u22a5 could be derived from previous goal (Eg X) using \u00acE, \n if \u00acX had already been given or derived. \u00acE backwards \nallows you to select back a previous derived or given formula \n\u00acX and generates X as the new goal." |
public static final java.lang.String |
notnot |
"For example \u00ac\u00acP." |
public static final java.lang.String |
or |
"For example P \u2228 Q" |
public static final java.lang.String |
or_introduction_backwards |
"Since you have a disjunction as a goal, you can\nassume that one of the sides is true and therefore\nuse it as your new goal, pressing either left or\nright will display the corresponding formula as\nyour new goal." |
public static final java.lang.String |
or_introduction_forwards |
"On which side of the disjunction should the current\ngoal appear?\n__________________________________________\n\nIn effect, you are specifying the formula from which\nyour current goal can be derived by \u2228 introduction.\nThis step is not often used, refer to the heuristics.\n\n" |
public static final java.lang.String |
pc |
"Input the conclusion you would like to be derived by PC Introduction Forwards\n________________________________________________________________________________\n\nHint: If you want to use this rule to derive x (the formula you are asked\nto input in this screen) you will have to complete the proof from \u00acx to \u22a5.\n\n" |
public static final java.lang.String |
reflexivity_forwards |
"Input the term you would like to apply reflexivity to\n_____________________________________________________\n\nHint: Provided a constant exists in your signature,\napplying reflexivity to it will produce a new goal\nline of the form a = a or with function symbols such\nas P(a) = P(a)\n\n" |
public static final java.lang.String |
reflexivity_forwards_no_constants |
"Input the term you would like to apply reflexivity to\n_____________________________________________________\n\nHint: Provided a constant exists in your signature,\napplying reflexivity to it will produce a new goal\nline of the form a = a or with function symbols such\nas P(a) = P(a)\n\nIt appears that you do not have a constant in your\nsignature, to add a constant click on the Options\nmenu > add to signature > constants\n\nAt the top of the rules pane a text field will appear\nin which you can add a constant of your choice\n\n" |
public static final java.lang.String |
subs_backwards |
"For equality substitution backwards the goalline needs to be selected \nfirst then the equality say s1=s2, which is used to substitute the either\nthe occurences of s1 in the goal by s2 or vice versa. There will also be \nan option to replace all or enter the formula that must be the new goal,\nif there are multiple occurences of s1 or s2 in the goal." |
public static final java.lang.String |
subs_forwards |
"For equality susbstition forwards two equations need to be selected.\nThe first of the equations needs to be an equality, say s1=s2. When\nsubstituting the first equation into the second you will be given an\noption to replace all occurences of s1 in the second equation by s2 \nor vice versa and you will also be given an option to replace only the\nyou require to be replaced." |
public static final java.lang.String |
thereexist_elimination_forwards |
"Input the conclusion you\'d like to be derived by There Exists Elimination Forwards\n____________________________________________________________________________________\n\nHint: If you want to use this rule to derive \u2203x(P(x)) (the formula you are asked\nto input in this screen) you will have to complete the proof from P(sk1) to \u2203x(P(x))\n\n" |
public static final java.lang.String |
thereExists |
"For example \u2203P." |
public static final java.lang.String |
thereexists_introduction_forwards_optional |
"(Optionally) input the There Exists formula you\'d like to introduce\n_____________________________________________________________\n\nHint: if you have P(a,b) for example, you can deduce \u2203u(P(u,b)) or even\n\u2203u\u2203v(P(u,v)) for more help see the manual entry, for simple cases with one\nvariable click ok to skip to the next screen\n\n" |
public static final java.lang.String |
thereexists_introduction_forwards_specify |
"Specify the term to substitute the new Exists variable for\n___________________________________________\n\nHint: The term which you select in this screen must be in\nthe formula you selected and must be unbounded, the\nformula you selected will then be nested inside a \u2203\nformula, in the next screen you will need to specify\nthe name of the variable of the \u2203 formula\n\n" |
public static final java.lang.String |
thereexists_introduction_forwards_specify_input |
"Input the name of the new Exists variable\n______________________________\n\nHint: Entering z will display a \u2203z formula and\nall instances of the term you selected in\nthe previous screen will be replaced by the\nnew variable\n\n" |
public static final java.lang.String |
tm |
"TrustMe rule:\n\nForwards:\n1. Select an empty line and click TM\n2. You may now select the lines that you have used for\nthe justification of inserting a new formula\n3. Type the formula you would like to add to the proof\n\nBackwards:\n1. Select a goal line and click TM\n2. You may now select the lines that you have used for\nthe justification of inserting a new goal\n3. Type the formula you would like to add to the proof\nas the new goal, the formula will then appear along with\nthe line numbers which were used as justification." |
public static final java.lang.String |
tm_backwards |
"TrustMe rule:\n\nYou are using this rule backwards:\n1. You may now select the lines that you have used for\nthe justification of inserting a new goal\n2. Type the formula you would like to add to the proof\nas the new goal, the formula will then appear along with\nthe line numbers which were used as justification.\n\nFor other uses click the help button" |
public static final java.lang.String |
tm_forwards |
"TrustMe rule:\n\nYou are using this rule forwards:\n1. You may now select the lines that you have used for\nthe justification of inserting a new formula\n2. Type the formula you would like to add to the proof" |
public static final java.lang.String |
tm_tick |
"TrustMe-Tick rule:\n\nForwards:\nTM-Tick cannot be applied forwards\n\nBackwards:\n1. Select a goal line and click TM\u221a\n2. You may now select the lines of the proof that you\nhave used to justify or deduce that the goal line selected\nin step 1 follows on from the last proof line above it.\n3. The proof step and it\'s corresponding sub-proofs are\ncompleted, i.e. the empty line is removed and \"something\"\nwill turn green." |
public static final java.lang.String |
tm_tick_backwards |
"TrustMe-Tick rule:\n\n1. You may now select the lines of the proof that you\nhave used to justify or deduce that the goal line selected\nin step 1 follows on from the last proof line above it.\n2. The proof step and it\'s corresponding sub-proofs are\ncompleted, i.e. the empty line is removed and \"something\"\nwill turn green." |
public static final java.lang.String |
truth |
"For example \u22a4" |