Hilbert II - JAVA-Packages - Principia Mathematica II

com.meyling.principia.logic.rule
Interface Rule

All Superinterfaces:
Argument
All Known Implementing Classes:
AddAxiom, AddSentence, ApplyAxiom, ApplySentence, ConjunctionRule, ElementaryEquivalence, Generalization, HypotheticalSyllogism, LeftAddition, LeftAdditionConjunction, LeftAdditionEquivalence, LeftAdditionImplication, ModusPonens, Particularization, RenameBoundSubjectVariable, RenameFreeSubjectVariable, ReplacePredicateVariable, ReplacePropositionVariable, ReverseAbbreviation, ReverseImplication, RightAddition, RightAdditionConjunction, RightAdditionEquivalence, RightAdditionImplication, SubstLine, UseAbbreviation

public interface Rule
extends Argument

Every logical rule must implement this interface. Each rule makes it possible to extend a proof.

Version:
$Revision: 1.7 $
Author:
Michael Meyling

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

check

public void check(Module module,
                  ProofLineList proofLines,
                  int position,
                  Formula formula)
           throws ArgumentException
Check if proof could be extended with formula (using the arguments of rule).

Parameters:
module - the module context
proofLines - the 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

extendWithout

public ProofLineList extendWithout(Module module,
                                   ProofLineList proofLines,
                                   int position)
                            throws IllegalArgumentException
Return proof lines that could replace the proof line position.

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()
Get proof line numbers that are used to derive the new formula.

Returns:
numbers of involved proof lines

changeProofLines

public Rule changeProofLines(int[] mapping)
Get proof line numbers that are used to derive the new formula.

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

getVersion

public Version getVersion()
Get version of this rule.

Returns:
rule version

Hilbert II - JAVA-Packages - Principia Mathematica II

©left GNU General Public Licence
All Rights Reserved.