You are looking at historical revision 6727 of this page. It may differ significantly from its current revision.


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/ ...
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 (()))


You can see that both statements are logically valid.