You are looking at historical revision 6728 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.