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 HypotheticalSyllogism

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

All Implemented Interfaces:
  Argument, Rule

public class HypotheticalSyllogism
extends AbstractArgumentList
implements Argument, Rule

Implemention of (pure) Hypothetical Syllogism:

`A1 => A2`

`A2 => A3`

`---------`

`A1 => A3`

Version:
  $Revision: 1.12 $
Author:
  Michael Meyling

Constructor Summary
`HypotheticalSyllogism(Argument[] arguments)` Constructs a hypothetical syllogism 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 because of hypothetical syllogism.
`static void` | `checkDeclaration(Module module, RuleDeclaration declaration)` Check if 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

### HypotheticalSyllogism

    public HypotheticalSyllogism(Argument[] arguments)
                          throws ArgumentException

  Constructs a hypothetical syllogism rule.

Parameters:
  `arguments` - two line numbers to operate on first argument must reference an implication second argument must reference an implication that has the second argoument of the first referenced formula as the first argument
Throws:
  `ArgumentException` - if there are not exactly two arguments that are instances of `Counter` or these arguments are not bigger than zero

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 because of hypothetical syllogism.

  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 numbers are not allowed (e.g. between 1 and the minimum of `position` and current maximum proof line number) or the refrenced proof lines are no `Implication`s or the first part formula of the second proof line is not equal to the second part formula of the first proof line or the implication made by the first part of the first formula and the second part of the second formula is not equal to `formula` or a version conflict occurs

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

### checkDeclaration

    public static final void checkDeclaration(Module module,
                                              RuleDeclaration declaration)
                                       throws ArgumentException

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