Orbital library

orbital.moon.logic.resolution
Class SaturationResolution

java.lang.Object
  extended by orbital.moon.logic.resolution.ResolutionBase
      extended by 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

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.