|
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.ReplacePredicateVariable
Replace predicate variable by a formula:
A[R(x,y,z)]
formula F(x,y,z)
------------------
A[F(x,y,z)]
Constructor Summary | |
ReplacePredicateVariable(Argument[] arguments)
Constructs a replace predicate variable rule. |
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 if replacing the predicate variable by the formula of the constructor. |
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 ReplacePredicateVariable(Argument[] arguments) throws ArgumentException
arguments
- ArgumentException
- if there are not three instances of
Counter
, PredicateVariable
,
Formula
(in exactly that order) or
the restrictions from above are not fullfilledMethod Detail |
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 add
ArgumentException
- if addition is not possible
because the proof line number is not allowed (e.g.
between 1 and the minimum of position
and current maximum proof line number)
or the referenced proof line is no formula
or the set of free variables of the formula and
the set of bound variables of the proof line
aren't disjunct
or the set of bound variables
of the formula and the subject variables of the
proof line aren't disjunct
or the predicate variable is in reach of an
quantor with subject variable x, and x
occurs in the replacement formula
or the resulting formula is not equal to
formula
or a version conflict occurspublic ProofLineList extendWithout(Module module, ProofLineList proofLines, int position) throws UnsupportedOperationException
Rule
position
.
extendWithout
in interface Rule
module
- the belonging moduleproofLines
- proof linesposition
- referenced proof line (starting with 0)
in proofLines
position
UnsupportedOperationException
- if this rule couldn't
be reduced at all because it is a basic rulepublic 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 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 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. |