Resolution implementation in Scheme?

[Panu Kalliokoski]

Hello all,

I'm currently writing my master's thesis on inductive logic, and as a
part of this, I've been writing a first order predicate logic library
for Scheme (I prefer to do this work in Scheme). However, my own
resolution procedure still has some bugs (such as not being able to
prove an arbitrary clause ?p from a knowledge base of (or ?x ?y)); and
since this resolution procedure seems very hard to get right and even
harder to get efficient, I would like to know whether you guys know of a
decent resolution implementation for Scheme that is available for public
download. I googled around and found an implementation in Haskell I
haven't evaluated and one in Common Lisp that sucked absolutely.

If there is some decent package for handling logic expressions in
Scheme, I'd very much like to learn about it and also see it added to
e.g. SLIB :) I guess one could be found in some theorem prover, but I'm
not familiar with them...

(On a related note but OT for the NG: does someone know some way to
check clauses generated by resolution so that resolving this KB does not
diverge: (or (p ?x ?y) (not (p ?x ?z)) (not (p ?z ?y))) with (not (p a
b)) ?)

thanks,
Panu

[Emilio Lopes]

Panu Kalliokoski writes:

> If there is some decent package for handling logic expressions in
> Scheme, I'd very much like to learn about it and also see it added
> to e.g. SLIB :)

Have you searched the Scheme Repository at Indiana University?

http://www.cs.indiana.edu/scheme-repository/SRhome.html

It is certainly worth a look!

--
Emílio C. Lopes Ich leb und weiß nit wie lang,
Munich, Germany ich stirb und weiß nit wann,
ich fahr und weiß nit wohin,
(Martinus von Biberach) mich wundert, dass ich fröhlich bin!

[zitterb...@gmail.com]

There doesn't seem to be anything there.

[Ben Goetter]

zitterb...@gmail.com wrote:
>> Have you searched the Scheme Repository at Indiana University?
>

> There doesn't seem to be anything there.

There are two implementations of Prolog in there: Cleary /et al/'s
ancient pure Prolog, and a very very old version of Dorai Sitaram's
Schelog. For a more recent Schelog, see
http://www.ccs.neu.edu/home/dorai/schelog/schelog.html - there, I just
saved you a G**gle.

The OP might also look at Kanren, http://kanren.sourceforge.net, though
I haven't dived into it myself (am waiting for a chance to read /The
Reasoned Schemer/ first).

Kanren requires R5RS. Schelog will run on R4RS + define-macro.
prolog1.2 requires only R4RS.

[Panu Kalliokoski]

I have found these, but I've become to understand that they only
implement "resolution" for Horn clause logic, while I'm looking for
resolution in full first-order predicate logic where negation is a true
connective.

Panu

[Panu Kalliokoski]

Panu Kalliokoski wrote:
> I'm currently writing my master's thesis on inductive logic, and as a
> part of this, I've been writing a first order predicate logic library
> for Scheme (I prefer to do this work in Scheme). However, my own
> resolution procedure still has some bugs (such as not being able to
> prove an arbitrary clause ?p from a knowledge base of (or ?x ?y));

An update: I now fixed this bug. I still find it hard to believe no
implementation for full FOL resolution is available in Scheme... I can
publish my code when it's more finished (you can also ask for the code
if you have some use for it).

Panu