Outdated egg!

This is an egg for CHICKEN 3, the unsupported old release. You're almost certainly looking for the CHICKEN 4 version of this egg, if it exists.

If it does not exist, there may be equivalent functionality provided by another egg; have a look at the egg index. Otherwise, please consider porting this egg to the current version of CHICKEN.



This egg is for doing predicate calculus, to see whether a statement in predicate calculus is logically valid or not. The algorithm is guaranteed to terminate if the statement can be proven. The algorithm is resolution based.

Supported Quantifiers and Logical Connectives


"exist"  means "there exists"
"all"    means "for all"

Logical Connectives:

xor and or not => <=>


For example, you want to know if this statement is logically valid:

(all y (=> (A y y) (exist x (A x y)))) 

You simply negate the statement like:

(not (all y (=> (A y y) (exist x (A x y))))) 

And then do a clausal form transformation:

(clausal-form '(not (all y (=> (A y y) (exist x (A x y)))))) 

And finally, a full resolution:

(full-resolution (clausal-form '(not (all y (=> (A y y) (exist x (A x y)))))))

You will either get a proof -- you will see "found" and then "(())" at the end of the list -- or the program might run forever.

Here is an example session:

 ;Version 2.732 - linux-unix-gnu-x86      [ symbolgc manyargs dload ptables applyhook cross ]
 ;(c)2000-2007 Felix L. Winkelmann        compiled 2007-11-06 on localhost (Linux)
 ;1> (use predicate-calculus)
 ; loading /usr/lib/chicken/3/predicate-calculus.so ...
 ;2> (full-resolution (clausal-form '(not (all y (=> (A y y) (exist x (A x y)))))))
 ;(((A skolem3 skolem3)) ((not (A ?x4 skolem3))) found clause-i ((A skolem3 skolem3)) clause-j ((not (A ?x4 skolem3))) resolution-set (()))

Here is a second example:

 ;3> (full-resolution (clausal-form '(not (=> (and (A x) (B x)) (A x)))))
 ;(((A x)) ((B x)) ((not (A x))) found clause-i ((A x)) clause-j ((not (A x))) resolution-set (()))


Naruto Canada narutocanada@gmail.com




Read more about Predicate calculus with equality here:

With code snippets from:



Version History