
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
java.lang.Object orbital.moon.logic.resolution.ResolutionBase
public abstract class ResolutionBase
Basic skeleton for resolution theorem provers.
General resolution procedure for M_{1},...,M_{n} ⊨ A is
R := E while □∉R do if there are clauses C_{1},C_{2}∈R, and a variable renaming ρ with Resolvent(C_{1}, ρ(C_{2})) ∉ R then choose such clauses C_{1},C_{2}∈R, and choose such a variable renaming ρ R := R∪{Resolvent(C_{1}, ρ(C_{2}))} else return fail fi end return success
Constructor Summary  

ResolutionBase()

Method Summary  

protected static ClausalFactory 
getClausalFactory()

boolean 
infer(Formula[] B,
Formula D)
Apply the inference relation ~ according to the implementation calculus K. 
boolean 
isComplete()
Whether the calculus K underlying this object to implement the inference relation is complete. 
boolean 
isSound()
Whether the calculus K underlying this object to implement the inference relation is sound. 
protected abstract boolean 
prove(ClausalSet knowledgebase,
ClausalSet query)
Try to prove or disprove the conjecture. 
void 
setVerbose(boolean newVerbose)
Add verbosity, i.e. 
Methods inherited from class java.lang.Object 

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

public ResolutionBase()
Method Detail 

protected static ClausalFactory getClausalFactory()
public void setVerbose(boolean newVerbose)
public boolean infer(Formula[] B, Formula D)
infer
in interface Inference
B
 the premises, i.e. basic knowledge formulas assumed true for the inference.
Use an array of length 0
or null
to denote the inference
"∅ ~ w"
from the empty set of knowledge ∅. Only axioms are available then, and thus the result
is equal to that of "true
~ d".
This inference from the empty set is abbreviated as "~ w"
because it will only infer tautologies.D
 the conclusion claimed, i.e. the formula to deduce from w, if possible.
public boolean isSound()
Inference
isSound
in interface Inference
public boolean isComplete()
Inference
isComplete
in interface Inference
protected abstract boolean prove(ClausalSet knowledgebase, ClausalSet query)
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.

Orbital library 1.3.0: 11 Apr 2009 

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 