org.qedeq.kernel.bo.logic.proof.finder
Class ProofFinderImpl

java.lang.Object
  org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImpl

All Implemented Interfaces:

ProofFinder

public class ProofFinderImpl
extends java.lang.Object
implements ProofFinder

Find basic proofs for formulas.

Author:

Michael Meyling

Constructor Summary

ProofFinderImpl()
Constructor.

Method Summary

void	findProof(Element formula, FormalProofLineList proof, ModuleContext context, Parameters parameters, ModuleLogListener log, Element2Utf8 trans) Finds a formal proof.
java.lang.String	getExecutionActionDescription() Get a description which action is currently taken.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ProofFinderImpl

public ProofFinderImpl()

Constructor.

Method Detail

findProof

public void findProof(Element formula,
                      FormalProofLineList proof,
                      ModuleContext context,
                      Parameters parameters,
                      ModuleLogListener log,
                      Element2Utf8 trans)
               throws ProofException,
                      InterruptException

Description copied from interface: ProofFinder

Finds a formal proof.

Specified by:

findProof in interface ProofFinder

Parameters:

formula - Formula we want to proof.

proof - Initial proof lines containing only "Add" lines.

context - We are in this context.

parameters - Further parameters to tune search process.

log - Log progress.

trans - Transformer for getting UTF-8 out of elements.

Throws:

ProofException - Finding result.

InterruptException - Proof finding was interrupted.

getExecutionActionDescription

public java.lang.String getExecutionActionDescription()

Description copied from interface: ProofFinder

Get a description which action is currently taken.

Specified by:

getExecutionActionDescription in interface ProofFinder

Returns:

Description.