Propositional Clausal Logic in Oz

Okay,

Just a little update. I wanted to see how one could implement a model searcher/theorem prover in Oz. I found some very useful presentation slides for Declarative Programming by Coen De Roover at:

http://prog.vub.ac.be/~cderoove/declarative_programming/

 Which I use as a guide for what I am trying to accomplish. Up to now, I have managed to create a PCL model searcher that can do proof by refutation using resolution. Here is some spoiler code:

% Set up a new Propositional Clausal Logic Knowledge base


PCLKB = {New KnowledgeBase init(PCL)}


% Assert some facts in it.


{List.forAll
 [
  [happy ':-' has_friends]
  [friendly ':-' happy]
  [wet ':-' rains]
  [':-' wet]
 ]
 proc {$ I}
    {PCLKB assert(I)}
 end
}


% Prove takes place with resolution by refutation


{List.forAll
 [
  [friendly ':-' has_friends]
  [friendly]
  [':-' rains]
 ]
 proc {$ I}
    {Browse prove(I)}
    {Browse
     {PCLKB prove(I $)}
    }
 end
}

and the necessary browser output:

prove([friendly ':-' has_friends])
true
prove([friendly])
false
prove([':-' rains])
true

For the moment, I will move to relational clausal logic so I am not going to bother with fixing up and releasing the code, unless someone asks for it of course.