|
Hilbert II - JAVA-Packages - Principia Mathematica II | ||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
Every logical rule must implement this interface. Each rule makes it possible to extend a proof.
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 (using the arguments of rule). |
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. |
Methods inherited from interface com.meyling.principia.argument.Argument |
containsPatternVariables, copy, create, equals, getArgument, getArgumentSize, getPatternVariables, getReplacementParents, getSearchParents, hashCode, matches, matches, replace, replace, replace, replaceMatches, toString |
Method Detail |
public void check(Module module, ProofLineList proofLines, int position, Formula formula) throws ArgumentException
module
- the module contextproofLines
- the proof linesposition
- number of proof lines that could be used
in the ruleformula
- formula to add
ArgumentException
- if addition is not possiblepublic ProofLineList extendWithout(Module module, ProofLineList proofLines, int position) throws IllegalArgumentException
position
.
module
- the belonging moduleproofLines
- proof linesposition
- referenced proof line (starting with 0)
in proofLines
position
IllegalArgumentException
- if extension is impossible
or other problems occured
if the module was checked before, this exception
could only occur if there is an programming error
UnsupportedOperationException
- if this rule couldn't
be reduced at all because it is a basic rulepublic int[] getProofLines()
public Rule changeProofLines(int[] mapping)
mapping
- array that maps old proof line numbers (index) to
new ones (value)
IllegalArgumentException
- if a needed value is -1public Version getVersion()
|
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. |