orbital.moon.logic.resolution
Class SetOfSupportResolution

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

All Implemented Interfaces:

Inference

public class SetOfSupportResolution
extends ResolutionBase

Direct set of support resolution.

Author:

André Platzer

Constructor Summary

SetOfSupportResolution()

Method Summary

protected void	deletion(ClausalSet newResolvents, ClausalSet usable, ClausalSet setOfSupport) Delete superfluous clauses.
protected boolean	prove(ClausalSet knowledgebase, ClausalSet query) Try to prove or disprove the conjecture.
protected Clause	selectClause(ClausalSet S) Perform a fair selection of one clause out of S.

Methods inherited from class orbital.moon.logic.resolution.ResolutionBase

getClausalFactory, infer, isComplete, isSound, setVerbose

Methods inherited from class java.lang.Object

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

Constructor Detail

SetOfSupportResolution

public SetOfSupportResolution()

Method Detail

selectClause

protected Clause selectClause(ClausalSet S)

Perform a fair selection of one clause out of S. Removes the selected clause from S.

Preconditions:

!S.isEmpty()

Postconditions:

OLD(S) = {RES} union S

deletion

protected void deletion(ClausalSet newResolvents,
                        ClausalSet usable,
                        ClausalSet setOfSupport)

Delete superfluous clauses. Apply any deletion strategies to the specified sets of clauses R, U and S.

Parameters:

newResolvents - the new resolvents just resolved most recently.

usable - the set of usable clauses in the knowledgebase which are not in the set of support.

setOfSupport - the current set of support prior to adding newResolvents.

prove

protected boolean prove(ClausalSet knowledgebase,
                        ClausalSet query)

Description copied from class: ResolutionBase

Try to prove or disprove the conjecture.

Specified by:

prove in class ResolutionBase

Parameters:

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

query - the initial set of support.

Returns:

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

See Also:

Template Method

Preconditions:

knowledgebase is satisfiable