Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| Hilbert II - JAVA-Packages - Principia Mathematica II
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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.