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

# Contributions

Read more about Predicate calculus with equality here:

With code snippets from:

None