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

## Author

Naruto Canada narutocanada@gmail.com

MIT

## Contributions (claimed your stolen codes or stolen ideas here)

; Read more about Predicate calculus with equality here
; us.metamath.org/index.html
; www.mathsci.appstate.edu/~jlh/primer/hirst.pdf
; www.enm.bris.ac.uk/research/aigroup/enjl/logic/sld034.htm
; www.cs.mu.oz.au/255/lec/subject-prop_resolution.pdf
;
; With code snippets from
; comp.lang.scheme
; mitpress.mit.edu/sicp/full-text/book/book.html
; www.ccs.neu.edu/home/dorai/t-y-scheme/t-y-scheme.html
; www-swiss.ai.mit.edu/~jaffer/SCM.html
; www.cis.temple.edu/~ingargio/cis587/readings/clausal-alg.cl
; bit-scheme

None