orbital.moon.logic.resolution
Class ResolutionBase

java.lang.Object
  orbital.moon.logic.resolution.ResolutionBase

All Implemented Interfaces:

Inference

Direct Known Subclasses:

SaturationResolution, SearchResolution, SetOfSupportResolution

public abstract class ResolutionBase
extends java.lang.Object
implements Inference

Basic skeleton for resolution theorem provers.

General resolution procedure for M₁,...,M_n ⊨ A is

1. E := {Cl_∀M₁,...,Cl_∀M₁,¬Cl_∀A}
2. transform each formula in E to prenex normal form
3. transform each formula in E to Skolem normal form with matrices in conjunctive normal form. The Skolem-functions introduced are new and distinct.
4. drop the ∀-quantifiers and write the remaining conjunctions of disjunctions of literals as sets of clauses. The union of these clauses is (again) called E.
5. try to resolve from E (with building variants to achieve disjunct variables) the empty clause □. Use a refinement or stronger variant of the following nondeterministic procedure:

        R := E
        while □∉R do
            if there are clauses C1,C2∈R, and a variable renaming ρ
                    with Resolvent(C1, ρ(C2)) ∉ R
            then
                choose such clauses C1,C2∈R, and
                choose such a variable renaming ρ
                R := R∪{Resolvent(C1, ρ(C2))}
            else
                return fail
            fi
        end
        return success
        

Author:

André Platzer

Constructor Summary

ResolutionBase()

Method Summary

protected static ClausalFactory	getClausalFactory()
boolean	infer(Formula[] B, Formula D) Apply the inference relation |~ according to the implementation calculus K.
boolean	isComplete() Whether the calculus K underlying this object to implement the inference relation is complete.
boolean	isSound() Whether the calculus K underlying this object to implement the inference relation is sound.
protected abstract boolean	prove(ClausalSet knowledgebase, ClausalSet query) Try to prove or disprove the conjecture.
void	setVerbose(boolean newVerbose) Add verbosity, i.e.

Methods inherited from class java.lang.Object

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

Constructor Detail

ResolutionBase

public ResolutionBase()

Method Detail

getClausalFactory

protected static ClausalFactory getClausalFactory()

setVerbose

public void setVerbose(boolean newVerbose)

Add verbosity, i.e. print out a proof tree.

infer

public boolean infer(Formula[] B,
                     Formula D)

Apply the inference relation |~ according to the implementation calculus K.

Specified by:

infer in interface Inference

Parameters:

B - the premises, i.e. basic knowledge formulas assumed true for the inference. Use an array of length 0 or null to denote the inference "∅ |~ w" from the empty set of knowledge ∅. Only axioms are available then, and thus the result is equal to that of "true |~ d". This inference from the empty set is abbreviated as "|~ w" because it will only infer tautologies.

D - the conclusion claimed, i.e. the formula to deduce from w, if possible.

Returns:

whether w |~ d, that is whether d can be inferred from the facts in w, or not.

See Also:

Template Method

isSound

public boolean isSound()

Description copied from interface: Inference

Whether the calculus K underlying this object to implement the inference relation is sound.

The calculus K is

sound

if |~ ⊆ |≈, i.e. if W |~ F implies W |≈ F.

Specified by:

isSound in interface Inference

isComplete

public boolean isComplete()

Description copied from interface: Inference

Whether the calculus K underlying this object to implement the inference relation is complete.

The calculus K is

complete

if |≈ ⊆ |~, i.e. if W |≈ F implies W |~ F.

Specified by:

isComplete in interface Inference

prove

protected abstract boolean prove(ClausalSet knowledgebase,
                                 ClausalSet query)

Try to prove or disprove the conjecture.

Parameters:

knowledgebase - knowledge base W assumed consistent. W is kept in clausal normal form, and thus contains sets of literals.

query - the query &lnot;D, i.e. negated goal D forming the initial set of support.

Returns:

whether W ¬ &lnot;D is inconsistent, i.e. W |~ D holds.