|
Hilbert II - JAVA-Packages - Principia Mathematica II | ||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectcom.meyling.principia.argument.AbstractArgument
com.meyling.principia.argument.AbstractArgumentList
com.meyling.principia.logic.rule.ElementaryEquivalence
Implemention of using an elementary equivalence:
a => b
b => a
A(a)
---------
A(b)
Constructor Summary | |
ElementaryEquivalence(Argument[] arguments)
Constructs an elementary equivalence rule by two sentence references and an occurence number. |
Method Summary | |
Rule |
changeProofLines(int[] mapping)
Get proof line numbers that are used to derive the new formula. |
void |
check(Module module,
ProofLineList proofLines,
int position,
Formula formula)
Check if proof could be extended with formula. |
static void |
checkDeclaration(Module module,
RuleDeclaration declaration)
Check this rule could be declared. |
Argument |
create(Argument[] arguments)
Create a new Argument with given arguments. |
ProofLineList |
extendWithout(Module module,
ProofLineList proofLines,
int position)
Return proof lines that could replace the proof line position . |
int[] |
getProofLines()
Get proof line numbers that are used to derive the new formula. |
Version |
getVersion()
Get version of this rule. |
String |
toString()
Get the argument in String form. |
Methods inherited from class com.meyling.principia.argument.AbstractArgumentList |
copy, getArgument, getArgumentSize |
Methods inherited from class com.meyling.principia.argument.AbstractArgument |
containsPatternVariables, equals, getHighestNumber, getPatternVariables, getReplacementParents, getSearchParents, hashCode, matches, matches, replace, replace, replace, replaceMatches |
Methods inherited from class java.lang.Object |
clone, finalize, getClass, notify, notifyAll, wait, wait, wait |
Methods inherited from interface com.meyling.principia.argument.Argument |
containsPatternVariables, copy, equals, getArgument, getArgumentSize, getPatternVariables, getReplacementParents, getSearchParents, hashCode, matches, matches, replace, replace, replace, replaceMatches |
Constructor Detail |
public ElementaryEquivalence(Argument[] arguments) throws ArgumentException
arguments
- proof line reference, sentence references
and occurence
ArgumentException
- if there are not exactly four
arguments or the first argument is no instance of
Counter
(>0) or the second and the third arguments
are no instances
of LinkLabel
or the fourth argument is
no instance of an Counter
(>0)Method Detail |
public final void check(Module module, ProofLineList proofLines, int position, Formula formula) throws ArgumentException
formula
is equivalent to the referenced sentence
formula.
check
in interface Rule
module
- moduleproofLines
- proof linesposition
- number of proof lines that could be used
in the ruleformula
- formula to add
ArgumentException
- if formula
is not
equal to the formula referenced by this object
or a version conflict occurspublic static final void checkDeclaration(Module module, RuleDeclaration declaration) throws ArgumentException
module
- the module contextdeclaration
- the declaration that shall declare this rule
IllegalArgumentException
- if an programming error occured
ArgumentException
- if declaration failedpublic final ProofLineList extendWithout(Module module, ProofLineList proofLines, int position) throws IllegalArgumentException
position
.
extendWithout
in interface Rule
module
- the belonging moduleproofLines
- proof linesposition
- referenced proof line (starting with 0)
in proofLines
position
IllegalArgumentException
- if extension is impossible
or other problems occuredpublic int[] getProofLines()
Rule
getProofLines
in interface Rule
public Rule changeProofLines(int[] mapping)
Rule
changeProofLines
in interface Rule
mapping
- array that maps old proof line numbers (index) to
new ones (value)
public final Version getVersion()
Rule
getVersion
in interface Rule
public final Argument create(Argument[] arguments) throws ArgumentException
Argument
create
in interface Argument
create
in class AbstractArgumentList
ArgumentException
public final String toString()
Argument
String
form.
toString
in interface Argument
toString
in class AbstractArgumentList
|
Hilbert II - JAVA-Packages - Principia Mathematica II | ||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
©left GNU General Public Licence All Rights Reserved. |