org.qedeq.kernel.bo.logic.proof.common
Interface ProofFinder

All Known Implementing Classes:

ProofFinderImpl

public interface ProofFinder

A proof finder can create formal proofs for propositions.

Author:

Michael Meyling

Method Summary

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

Method Detail

findProof

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

Finds a formal proof.

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.

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

Throws:

InterruptException - Proof finding was interrupted.

ProofException - Finding result.

getExecutionActionDescription

java.lang.String getExecutionActionDescription()

Get a description which action is currently taken.

Returns:

Description.