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
Class ElementaryEquivalence

    java.lang.Object
      com.meyling.principia.argument.AbstractArgument
          com.meyling.principia.argument.AbstractArgumentList
              com.meyling.principia.logic.rule.ElementaryEquivalence

All Implemented Interfaces:
  Argument, Rule

public class ElementaryEquivalence
extends AbstractArgumentList
implements Argument, Rule

Implemention of using an elementary equivalence:

`a => b` `b => a` `A(a)` `---------`

`A(b)`

Version:
  $Revision: 1.15 $
Author:
  Michael Meyling

Constructor Summary
`ElementaryEquivalence(Argument[] arguments)` Constructs an elementary equivalence rule by two sentence references and an occurence number.

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.
`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

### ElementaryEquivalence

    public ElementaryEquivalence(Argument[] arguments)
                          throws ArgumentException

  Constructs an elementary equivalence rule by two sentence references and an occurence number.

Parameters:
  `arguments` - proof line reference, sentence references and occurence
Throws:
  `ArgumentException` - if there are not exactly four arguments or the first argument is no instance of `Counter` (>0) or the second and the third arguments are no instances of `LinkLabel` or the fourth argument is no instance of an `Counter` (>0)

Method Detail

### check

    public final void check(Module module,
                            ProofLineList proofLines,
                            int position,
                            Formula formula)
                     throws ArgumentException

  Check if proof could be extended with formula. This is true if `formula` is equivalent to the referenced sentence formula.

  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 `formula` is not equal to the formula referenced by this object or a version conflict occurs

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

### extendWithout

    public final ProofLineList extendWithout(Module module,
                                             ProofLineList proofLines,
                                             int position)
                                      throws IllegalArgumentException

  Return proof lines that could replace the proof line `position`.

  Specified by:
    `extendWithout` in interface `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

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

### getVersion

    public final Version getVersion()

  Description copied from interface: `Rule`
  Get version of this rule.

  Specified by:
    `getVersion` in interface `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`
  Specified by:
    `create` in class `AbstractArgumentList`
  Throws:
    `ArgumentException`

### toString

    public final String toString()

  Description copied from interface: `Argument`
  Get the argument in `String` form.

  Specified by:
    `toString` in interface `Argument`
  Specified by:
    `toString` in class `AbstractArgumentList`

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.