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 ConjunctionRule

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

All Implemented Interfaces:
  Argument, Rule

public class ConjunctionRule
extends AbstractArgumentList
implements Argument, Rule

Implemention of conjunction rule:

`A1`

`A2`

`---------`

`A1 & A2`

Version:
  $Revision: 1.10 $
Author:
  Michael Meyling

Constructor Summary
`ConjunctionRule(Argument[] arguments)` Constructs a conjunction 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 conjunction rule.
`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

### ConjunctionRule

    public ConjunctionRule(Argument[] arguments)
                    throws ArgumentException

  Constructs a conjunction rule.

Parameters:
  `arguments` - two line numbers to operate on both arguments could reference any formula but the conjunction of both formulas must be a formula too
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 conjunction rule.

  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 second proof line is no `Implication` or the first part formula of the second proof line is not equal to the first proof line or the second part formula of the second proof line 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`
  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:
    `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`
  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 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.