|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectorg.qedeq.kernel.bo.logic.proof.finder.ProofFinderImpl
public class ProofFinderImpl
Find basic proofs for formulas.
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 |
---|
public ProofFinderImpl()
Method Detail |
---|
public void findProof(Element formula, FormalProofLineList proof, ModuleContext context, Parameters parameters, ModuleLogListener log, Element2Utf8 trans) throws ProofException, InterruptException
ProofFinder
findProof
in interface ProofFinder
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.
ProofException
- Finding result.
InterruptException
- Proof finding was interrupted.public java.lang.String getExecutionActionDescription()
ProofFinder
getExecutionActionDescription
in interface ProofFinder
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |