|
PMII - JAVA-Packages - Principia Mathematica II | |||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object | +--com.meyling.principia.argument.AbstractArgument | +--com.meyling.principia.argument.AbstractArgumentList | +--com.meyling.principia.logic.rule.RightAdditionEquivalence
Implemention of "addition" of an equivalence on the right side.
A1 => A2
A2 => A1
----------------------------
(A1 <=> A3) => (A2 <=> A3)
Constructor Summary | |
RightAdditionEquivalence(Argument[] arguments)
Constructs a left implication addition rule. |
Method Summary | |
(package private) static void |
Initialize version information. |
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 because of right addition of a implication. |
static void |
checkDeclaration(Module module,
RuleDeclaration declaration)
Check if 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 RightAdditionEquivalence(Argument[] arguments) throws ArgumentException
arguments
- ArgumentException
- if there are not exactly three
arguments, if the first two arguments are not
instances of Counter
or are not bigger than zero, or
if the third argument is no instance of a Formula
Method Detail |
static void()
public final void check(Module module, ProofLineList proofLines, int position, Formula formula) throws ArgumentException
check
in interface Rule
module
- moduleproofLines
- proof linesposition
- number of proof lines that could be used
in the ruleformula
- formula to addArgumentException
- if addition is not possible
because the proof line numbers are not allowed (e.g.
between 0 and the minimum of position - 1
and current maximum proof line number)
or the proof line number is no Implication
or the implication and the additional formula have
in common a subject variable that is bound in one
formula and free in the other,
or the resulting formula is not equal to
formula
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 ruleIllegalArgumentException
- if an programming error occuredArgumentException
- 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 final int[] getProofLines()
Rule
getProofLines
in interface Rule
com.meyling.principia.logic.rule.Rule
public final Rule changeProofLines(int[] mapping)
Rule
changeProofLines
in interface Rule
com.meyling.principia.logic.rule.Rule
mapping
- array that maps old proof line numbers (index) to
new ones (value)IllegalArgumentException
- if a needed value is -1public final Version getVersion()
Rule
getVersion
in interface Rule
com.meyling.principia.logic.rule.Rule
public final Argument create(Argument[] arguments) throws ArgumentException
Argument
create
in interface Argument
create
in class AbstractArgumentList
com.meyling.principia.argument.Argument
arguments
- with these arguments the operator should
be createdArgumentException
- if creation failedpublic final String toString()
Argument
String
form.toString
in interface Argument
toString
in class AbstractArgumentList
com.meyling.principia.argument.Argument
|
PMII - JAVA-Packages - Principia Mathematica II | |||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
©left GNU General Public Licence All Rights Reserved. |