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

## 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>

You can see that both statements are logically valid.