orbital.moon.logic.resolution
Class SearchResolution

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

All Implemented Interfaces:

Inference

public class SearchResolution
extends ResolutionBase

Set of support resolution based on search.

Author:

André Platzer

Constructor Summary

SearchResolution()

Method Summary

protected boolean

prove(ClausalSet knowledgebase, ClausalSet query) Try to prove or disprove the conjecture.

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

SearchResolution

public SearchResolution()

Method Detail

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:

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.