Note: This is taken from the Chicken Wiki, where a more recent version could be available.

Introduction

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

Quantifiers:

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

Logical Connectives:

xor and or not => <=>

Examples

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:

 ;CHICKEN
 ;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 (()))
 ;3>

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 (()))
 ;4>

Author

Naruto Canada narutocanada@gmail.com

License

MIT

Contributions

Read more about Predicate calculus with equality here:

With code snippets from:

Requirements

None

predicate-calculus