org.qedeq.kernel.bo.logic.common
Interface ReferenceResolver

All Known Implementing Classes:

FormalProofCheckerExecutor, ProofChecker2Impl

public interface ReferenceResolver

Resolver for references from formal proof lines. Specific to a certain formal proof.

Author:

Michael Meyling

Method Summary

Element	getNormalizedFormula(Element element) Get formula in a normalized format.
Element	getNormalizedLocalProofLineReference(java.lang.String reference) Get local for proof line reference.
Element	getNormalizedReferenceFormula(java.lang.String reference) Get reference formula in a normalized format.
ModuleContext	getReferenceContext(java.lang.String reference) Module context for proof line reference.
boolean	isLocalProofLineReference(java.lang.String reference) Is this a local proof line reference?
boolean	isProvedFormula(java.lang.String reference) Check if a reference is a proved formula.

Method Detail

isProvedFormula

boolean isProvedFormula(java.lang.String reference)

Check if a reference is a proved formula.

Parameters:

reference - Reference to axiom, definition or proposition.

Returns:

Reference has a proved formula.

getNormalizedReferenceFormula

Element getNormalizedReferenceFormula(java.lang.String reference)

Get reference formula in a normalized format.

Parameters:

reference - Reference to axiom, definition or proposition.

Returns:

Already proved formula.

getNormalizedFormula

Element getNormalizedFormula(Element element)

Get formula in a normalized format.

Parameters:

element - Local formula to normalize.

Returns:

Normalized formula.

isLocalProofLineReference

boolean isLocalProofLineReference(java.lang.String reference)

Is this a local proof line reference?

Parameters:

reference - Local proof line reference to check for.

Returns:

Is this a local proof line reference for the caller?

getNormalizedLocalProofLineReference

Element getNormalizedLocalProofLineReference(java.lang.String reference)

Get local for proof line reference.

Parameters:

reference - Local proof line reference to check for.

Returns:

Local proof line for the caller. Might be null.

getReferenceContext

ModuleContext getReferenceContext(java.lang.String reference)

Module context for proof line reference.

Parameters:

reference - Local proof line reference to check for.

Returns:

Local proof line reference for the caller. Might be null.