PMII - JAVA-Packages - Principia Mathematica II

com.meyling.principia.logic.rule
Class RenameFreeSubjectVariable

java.lang.Object
  |
  +--com.meyling.principia.argument.AbstractArgument
        |
        +--com.meyling.principia.argument.AbstractArgumentList
              |
              +--com.meyling.principia.logic.rule.RenameFreeSubjectVariable
All Implemented Interfaces:
Argument, Rule

public class RenameFreeSubjectVariable
extends AbstractArgumentList
implements Argument, Rule

Replace a free subject variable by another subject variable:

A[x]

x is free in A[x]

y is not bound in A[x]

----------------------

A[y]

Version:
$Revision: 1.5 $
Author:
Michael Meyling

Constructor Summary
RenameFreeSubjectVariable(Argument[] arguments)
          Constructs a replace predicate variable 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 by replacing a free subject variable of a proof line by another subject variable.
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

RenameFreeSubjectVariable

public RenameFreeSubjectVariable(Argument[] arguments)
                          throws ArgumentException
Constructs a replace predicate variable rule.
Parameters:
arguments -
  • 0:Counter, as proof line reference (>0)
  • 1: subject variable
  • 2: another subject variable
Throws:
ArgumentException - if there are not exactly three arguments or the arguments are no instances of Counter, SubjectVariable, SubjectVariable in exactly this order.
Method Detail

static void ()
Initialize version information.

check

public final void check(Module module,
                        ProofLineList proofLines,
                        int position,
                        Formula formula)
                 throws ArgumentException
Check if proof could be extended with formula by replacing a free subject variable of a proof line by another subject variable.
Specified by:
check in interface Rule
Parameters:
module - module
proofLines - proof lines
position - number of proof lines that could be used in the rule
formula - formula to add
Throws:
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 does not contain the free subject variable that shall be found or the replacement subject variable is already an bound subject variable of the proof line or the resulting formula is not equal to formula or a version conflict occurs

extendWithout

public ProofLineList extendWithout(Module module,
                                   ProofLineList proofLines,
                                   int position)
                            throws UnsupportedOperationException
Description copied from interface: Rule
Return proof lines that could replace the proof line position.
Specified by:
extendWithout in interface Rule
Following copied from interface: com.meyling.principia.logic.rule.Rule
Parameters:
module - the belonging module
proofLines - proof lines
position - referenced proof line (starting with 0) in proofLines
Returns:
proof lines that could substitute the single proof line position
Throws:
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 rule

getProofLines

public int[] getProofLines()
Description copied from interface: Rule
Get proof line numbers that are used to derive the new formula.
Specified by:
getProofLines in interface Rule
Following copied from interface: com.meyling.principia.logic.rule.Rule
Returns:
numbers of involved proof lines

changeProofLines

public Rule changeProofLines(int[] mapping)
Description copied from interface: Rule
Get proof line numbers that are used to derive the new formula.
Specified by:
changeProofLines in interface Rule
Following copied from interface: com.meyling.principia.logic.rule.Rule
Parameters:
mapping - array that maps old proof line numbers (index) to new ones (value)
Returns:
same rule but with changed numbers of involved proof lines
Throws:
IllegalArgumentException - if a needed value is -1

checkDeclaration

public static final void checkDeclaration(Module module,
                                          RuleDeclaration declaration)
                                   throws ArgumentException
Check this rule could be declared.
Parameters:
module - the module context
declaration - the declaration that shall declare this rule
Throws:
IllegalArgumentException - if an programming error occured
ArgumentException - if declaration failed

getVersion

public final Version getVersion()
Description copied from interface: Rule
Get version of this rule.
Specified by:
getVersion in interface Rule
Following copied from interface: com.meyling.principia.logic.rule.Rule
Returns:
rule version

create

public final Argument create(Argument[] arguments)
                      throws ArgumentException
Description copied from interface: Argument
Create a new Argument with given arguments.
Specified by:
create in interface Argument
Overrides:
create in class AbstractArgumentList
Following copied from interface: com.meyling.principia.argument.Argument
Parameters:
arguments - with these arguments the operator should be created
Returns:
new constructed Argument
Throws:
ArgumentException - if creation failed

toString

public final String toString()
Description copied from interface: Argument
Get the argument in String form.
Specified by:
toString in interface Argument
Overrides:
toString in class AbstractArgumentList
Following copied from interface: com.meyling.principia.argument.Argument
Returns:
readable formula

PMII - JAVA-Packages - Principia Mathematica II

©left GNU General Public Licence
All Rights Reserved.