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.16 $
- Author:
- Michael Meyling
Constructor Summary |
Proposition(Argument[] arguments)
Constructs a mathematical proposition with its proof. |
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 interface com.meyling.principia.argument.Argument |
containsPatternVariables, copy, equals, getArgument, getArgumentSize, getPatternVariables, getReplacementParents, getSearchParents, hashCode, matches, matches, replace, replace, replace, replaceMatches |
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
.
check
public final void check(Module module,
String label)
throws ArgumentException
- Check if proof is correct.
- Specified by:
check
in interface ParagraphCheck
- Parameters:
module
- modulelabel
- 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 referencesIllegalArgumentException
- 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 referencesUnsupportedOperationException
- if there is a rule
which couldn't yet be reduced to simper rules
because the reduction for that rule isn't
implementedIllegalArgumentException
- 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
correctposition
- 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
- Overrides:
create
in class AbstractDynamicArgumentList
- Following copied from interface:
com.meyling.principia.argument.Argument
- Parameters:
arguments
- with these arguments the operator should
be created- Returns:
- new constructed Argument
- Throws:
ArgumentException
- if creation failed
toString
public final String toString()
- Description copied from interface:
Argument
- Get the argument in
String
form.
- Specified by:
toString
in interface Argument
- Overrides:
toString
in class AbstractDynamicArgumentList
- Following copied from interface:
com.meyling.principia.argument.Argument
- Returns:
- readable formula