You can edit this page using wiki syntax for markup.

Article contents:== Outdated egg! This is an egg for CHICKEN 3, the unsupported old release. You're almost certainly looking for [[/eggref/4/predicate-calculus|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 [[https://wiki.call-cc.org/chicken-projects/egg-index-4.html|egg index]]. Otherwise, please consider porting this egg to the current version of CHICKEN. [[tags: 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) ; 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 === License MIT === Contributions Read more about Predicate calculus with equality here: * [[http://us.metamath.org/index.html]] * [[http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf]] * [[http://www.enm.bris.ac.uk/research/aigroup/enjl/logic/sld034.htm]] * [[http://www.cs.mu.oz.au/255/lec/subject-prop_resolution.pdf]] With code snippets from: * {{comp.lang.scheme}} * [[http://mitpress.mit.edu/sicp/full-text/book/book.html]] * [[http://www.ccs.neu.edu/home/dorai/t-y-scheme/t-y-scheme.html]] * [[http://www-swiss.ai.mit.edu/~jaffer/SCM.html]] * [[http://www.cis.temple.edu/~ingargio/cis587/readings/clausal-alg.cl]] * bit-scheme === Requirements None === Version History Description of your changes:

I would like to authenticate

Spam control

What do you get when you multiply 9 by 3?