Changeset 9049 in project


Ignore:
Timestamp:
02/26/08 22:03:08 (12 years ago)
Author:
sjamaan
Message:

Update predicate calculus' syntax a bit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • wiki/predicate-calculus

    r6749 r9049  
    3030=== Here is an example session:
    3131
    32 ;CHICKEN
    33 ;Version 2.732 - linux-unix-gnu-x86      [ symbolgc manyargs dload ptables applyhook cross ]
    34 ;(c)2000-2007 Felix L. Winkelmann        compiled 2007-11-06 on localhost (Linux)
    35 
    36 ;1> (use predicate-calculus)
    37 ; loading /usr/lib/chicken/3/predicate-calculus.so ...
    38 ;2> (full-resolution (clausal-form '(not (all y (=> (A y y) (exist x (A x y)))))))
    39 ;(((A skolem3 skolem3)) ((not (A ?x4 skolem3))) found clause-i ((A skolem3 skolem3)) clause-j ((not (A ?x4 skolem3))) resolution-set (()))
    40 ;3>
     32  ;CHICKEN
     33  ;Version 2.732 - linux-unix-gnu-x86      [ symbolgc manyargs dload ptables applyhook cross ]
     34  ;(c)2000-2007 Felix L. Winkelmann        compiled 2007-11-06 on localhost (Linux)
     35 
     36  ;1> (use predicate-calculus)
     37  ; loading /usr/lib/chicken/3/predicate-calculus.so ...
     38  ;2> (full-resolution (clausal-form '(not (all y (=> (A y y) (exist x (A x y)))))))
     39  ;(((A skolem3 skolem3)) ((not (A ?x4 skolem3))) found clause-i ((A skolem3 skolem3)) clause-j ((not (A ?x4 skolem3))) resolution-set (()))
     40  ;3>
    4141
    4242=== Here is a second example:
    4343
    44 ;3> (full-resolution (clausal-form '(not (=> (and (A x) (B x)) (A x)))))
    45 ;(((A x)) ((B x)) ((not (A x))) found clause-i ((A x)) clause-j ((not (A x))) resolution-set (()))
    46 ;4>
    47 
    48 
     44  ;3> (full-resolution (clausal-form '(not (=> (and (A x) (B x)) (A x)))))
     45  ;(((A x)) ((B x)) ((not (A x))) found clause-i ((A x)) clause-j ((not (A x))) resolution-set (()))
     46  ;4>
    4947
    5048== Author
     
    5856== Contributions
    5957
    60 ;; Read more about Predicate calculus with equality here:
    61 ;; us.metamath.org/index.html
    62 ;; www.mathsci.appstate.edu/~jlh/primer/hirst.pdf
    63 ;; www.enm.bris.ac.uk/research/aigroup/enjl/logic/sld034.htm
    64 ;; www.cs.mu.oz.au/255/lec/subject-prop_resolution.pdf
    65 ;;
    66 ;; With code snippets from:
    67 ;; comp.lang.scheme
    68 ;; mitpress.mit.edu/sicp/full-text/book/book.html
    69 ;; www.ccs.neu.edu/home/dorai/t-y-scheme/t-y-scheme.html
    70 ;; www-swiss.ai.mit.edu/~jaffer/SCM.html
    71 ;; www.cis.temple.edu/~ingargio/cis587/readings/clausal-alg.cl
    72 ;; bit-scheme
     58Read more about Predicate calculus with equality here:
     59
     60* [[http://us.metamath.org/index.html]]
     61* [[http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf]]
     62* [[http://www.enm.bris.ac.uk/research/aigroup/enjl/logic/sld034.htm]]
     63* [[http://www.cs.mu.oz.au/255/lec/subject-prop_resolution.pdf]]
     64
     65With code snippets from:
     66
     67* {{comp.lang.scheme}}
     68* [[http://mitpress.mit.edu/sicp/full-text/book/book.html]]
     69* [[http://www.ccs.neu.edu/home/dorai/t-y-scheme/t-y-scheme.html]]
     70* [[http://www-swiss.ai.mit.edu/~jaffer/SCM.html]]
     71* [[http://www.cis.temple.edu/~ingargio/cis587/readings/clausal-alg.cl]]
     72* bit-scheme
     73
    7374== Requirements
    7475
Note: See TracChangeset for help on using the changeset viewer.