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

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

public final class ProofFinderUtility
extends java.lang.Object

Utilities for proofs finders.

Author:

Michael Meyling

Method Summary

static java.lang.String	getUtf8Line(Element formula, Reason reason, int i, Element2Utf8 trans) Get UTF-8 representation of proof line.
static java.lang.String	getUtf8Line(java.util.List lines, java.util.List reasons, int i, Element2Utf8 trans) Get UTF-8 representation of proof line.
static FormalProofLineList	shortenProof(java.util.List lines, java.util.List reasons, ModuleLogListener log, Element2Utf8 trans) Shorten given formal proof.

Methods inherited from class java.lang.Object

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

Method Detail

shortenProof

public static FormalProofLineList shortenProof(java.util.List lines,
                                               java.util.List reasons,
                                               ModuleLogListener log,
                                               Element2Utf8 trans)

Shorten given formal proof.

Parameters:

lines - Lines of formulas.

reasons - Reasons for derivation of formula. Must be Add, MP or SubstPred.

log - For BO logging.

trans - Transformer (used for logging).

Returns:

Reduced formal proof.

getUtf8Line

public static java.lang.String getUtf8Line(java.util.List lines,
                                           java.util.List reasons,
                                           int i,
                                           Element2Utf8 trans)

Get UTF-8 representation of proof line.

Parameters:

lines - Proof line formulas.

reasons - Proof line reasons.

i - Proof line to print.

trans - Transformer to get UTF-8 out of a formula.

Returns:

UTF-8 display text for proof line.

getUtf8Line

public static java.lang.String getUtf8Line(Element formula,
                                           Reason reason,
                                           int i,
                                           Element2Utf8 trans)

Get UTF-8 representation of proof line.

Parameters:

formula - Proof line formula.

reason - Proof line reason.

i - Proof line number.

trans - Transformer to get UTF-8 out of a formula.

Returns:

UTF-8 display text for proof line.