com.meyling.principia.logic.rule
Class ApplyAxiom

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

All Implemented Interfaces:

Argument, Rule

public class ApplyAxiom

extends AbstractArgumentList

implements Argument, Rule

Implementation of applying an Axiom:

A1 => A2

A3

---------

A4

if A1 => A2 matches A3 => A4

Version:

$Revision: 1.11 $

Author:

Michael Meyling

Constructor Summary

ApplyAxiom(Argument[] arguments)
Constructs an apply axiom rule by a proof line reference and an axiom reference.

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

ApplyAxiom

public ApplyAxiom(Argument[] arguments)
           throws ArgumentException

Constructs an apply axiom rule by a proof line reference and an axiom reference.

Parameters:

arguments - proof line reference, axiom reference

Throws:

ArgumentException - if there are not exactly two arguments or the arguments or if the first argument is not an instance of Counter or is not bigger than zero, or if the second argument is no instance of a LinkLabel

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 axiom 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 the implication made of the referenced proof line of this object and the formula of this object dosn't match the referenced axiom 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 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