orbital.moon.logic.resolution
Class SaturationResolution

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

All Implemented Interfaces:

Inference

public class SaturationResolution
extends ResolutionBase

Naïve saturation. Repeatedly adds all resolvents of the first clause with other clauses to the clausal set.

Author:

André Platzer

Constructor Summary

SaturationResolution()

Method Summary

protected void	deletion(ClausalSet newResolvents, ClausalSet setOfClauses) 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

SaturationResolution

public SaturationResolution()

Method Detail

selectClause

protected Clause selectClause(ClausalSet S)

Perform a fair selection of one clause out of S. Does not remove the selected clause from S.

Preconditions:

!S.isEmpty()

Postconditions:

OLD(S) = S ∧ RES∈S

deletion

protected void deletion(ClausalSet newResolvents,
                        ClausalSet setOfClauses)

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

Parameters:

newResolvents - the new resolvents just resolved most recently.

setOfClauses - the current set of clauses 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