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.paragraph
Class Proposition

    java.lang.Object
      com.meyling.principia.argument.AbstractArgument
          com.meyling.principia.argument.AbstractDynamicArgumentList
              com.meyling.principia.logic.paragraph.Proposition

All Implemented Interfaces:
  Argument, ParagraphCheck

public class Proposition
extends AbstractDynamicArgumentList
implements Argument, ParagraphCheck

Logical sentence.

Version:
  $Revision: 1.22 $
Author:
  Michael Meyling

Constructor Summary
`Proposition(Argument[] arguments)` Constructs a mathematical proposition with its proof.

Method Summary
`void` | `check(Module module, String label)` Check if proof is correct.
`void` | `compress()` Remove all double and unused proof lines.
`Argument` | `create(Argument[] arguments)` Create a new Argument with given arguments.
`void` | `reduceRuleVersion(Module module, Version version)` Reduce needed rule version and change proof lines in that way.
`void` | `replaceProofLineByProofLines(ProofLineList proofLines, int position)` Replace a single proof line by some (other) proof lines.
`String` | `toString()` Get the argument in `String` form.

Methods inherited from class com.meyling.principia.argument.AbstractDynamicArgumentList
`add, copy, getArgument, getArgumentSize, insert, remove, replace`

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

### Proposition

    public Proposition(Argument[] arguments)
                throws ArgumentException

  Constructs a mathematical proposition with its proof.

Parameters:
  `arguments` - sentence and its proof
Throws:
  `ArgumentException` - if there is not exactly two arguments or the first argument is not an instance of `Sentence` or the second argument is no instance of `ProofLineList`.

Method Detail

### check

    public final void check(Module module,
                            String label)
                     throws ArgumentException

  Check if proof is correct.

  Specified by:
    `check` in interface `ParagraphCheck`
  Parameters:
    `module` - module
    `label` - label of paragraph
  Throws:
    `ArgumentException` - if proof is not correct

### compress

    public final void compress()
                        throws ArgumentException

  Remove all double and unused proof lines.

  Throws:
    `ArgumentException` - if proof is there were any illegal line references
    `IllegalArgumentException` - if there was a programming error

### reduceRuleVersion

    public final void reduceRuleVersion(Module module,
                                        Version version)
                                 throws ArgumentException

  Reduce needed rule version and change proof lines in that way.

  Parameters:
    `module` - this is the connected module
  Throws:
    `ArgumentException` - if a proof line has major errors in their line references
    `UnsupportedOperationException` - if there is a rule which couldn't yet be reduced to simper rules because the reduction for that rule isn't implemented
    `IllegalArgumentException` - if there was a programming error

### replaceProofLineByProofLines

    public final void replaceProofLineByProofLines(ProofLineList proofLines,
                                                   int position)

  Replace a single proof line by some (other) proof lines. If the replacement lines are empty, nothing is done; by calling `compress` the caller could remove the proof line.

  Parameters:
    `proofLines` - these proof lines should be inserted, the line references must be already correct
    `position` - this line should be replaced by the new proof lines
  Throws:
    `IllegalArgumentException` - if `position` is not a valid one, or the remaping failed because the given proof lines had illegal references

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

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.