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

• egg

## predicate-calculus

### 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)
;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> ```

MIT