Orbital library

orbital.moon.logic.resolution
Class SetOfSupportResolution

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

Orbital library
1.3.0: 11 Apr 2009

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