Orbital library

orbital.moon.logic.resolution
Class ResolutionBase

java.lang.Object
  extended by orbital.moon.logic.resolution.ResolutionBase
All Implemented Interfaces:
Inference
Direct Known Subclasses:
SaturationResolution, SearchResolution, SetOfSupportResolution

public abstract class ResolutionBase
extends java.lang.Object
implements Inference

Basic skeleton for resolution theorem provers.

General resolution procedure for M1,...,Mn ⊨ A is

  1. E := {ClM1,...,ClM1,¬ClA}
  2. transform each formula in E to prenex normal form
  3. transform each formula in E to Skolem normal form with matrices in conjunctive normal form. The Skolem-functions introduced are new and distinct.
  4. drop the ∀-quantifiers and write the remaining conjunctions of disjunctions of literals as sets of clauses. The union of these clauses is (again) called E.
  5. try to resolve from E (with building variants to achieve disjunct variables) the empty clause □. Use a refinement or stronger variant of the following nondeterministic procedure:
         R := E
         while □∉R do
             if there are clauses C1,C2∈R, and a variable renaming ρ
                     with Resolvent(C1, ρ(C2)) ∉ R
             then
                 choose such clauses C1,C2∈R, and
                 choose such a variable renaming ρ
                 R := R∪{Resolvent(C1, ρ(C2))}
             else
                 return fail
             fi
         end
         return success
         

Author:
André Platzer

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

ResolutionBase

public ResolutionBase()
Method Detail

getClausalFactory

protected static ClausalFactory getClausalFactory()

setVerbose

public void setVerbose(boolean newVerbose)
Add verbosity, i.e. print out a proof tree.


infer

public boolean infer(Formula[] B,
                     Formula D)
Apply the inference relation |~ according to the implementation calculus K.

Specified by:
infer in interface Inference
Parameters:
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.
Returns:
whether w |~ d, that is whether d can be inferred from the facts in w, or not.
See Also:
Template Method

isSound

public boolean isSound()
Description copied from interface: Inference
Whether the calculus K underlying this object to implement the inference relation is sound.
The calculus K is
sound
if |~|≈, i.e. if W |~ F implies W |≈ F.

Specified by:
isSound in interface Inference

isComplete

public boolean isComplete()
Description copied from interface: Inference
Whether the calculus K underlying this object to implement the inference relation is complete.
The calculus K is
complete
if |≈|~, i.e. if W |≈ F implies W |~ F.

Specified by:
isComplete in interface Inference

prove

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

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.

Orbital library
1.3.0: 11 Apr 2009

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