source: project/release/2/predicate-calculus/predicate-calculus.html @ 8751

Last change on this file since 8751 was 8751, checked in by felix winkelmann, 14 years ago

rrb2 move completion

File size: 975 bytes
Line 
1<html>
2<body>
3;;<br>
4;; How to use predicate-calculus egg.<br>
5;;<br><br>
6
7(use predicate-calculus)<br><br>
8
9;;<br>
10;; For example, you want to know if this statement is logically valid:<br>
11;; (=> (and (A x) (B x)) (A x)) <br>
12;; Simply negate the statement and translate to clausal form, then do a full resolution. <br>
13;; You will either get a proof-- you will see "found" and then "(())" at the end of the list-- or the program will run forever.<br>
14;;<br><br>
15
16(full-resolution (clausal-form '(not (=> (and (A x) (B x)) (A x)) )))
17<br><br>
18(((A x)) ((B x)) ((not (A x))) found clause-i ((A x)) clause-j ((not (A x))) resolution-set (()))
19<br><br>
20;;<br>
21;; See the following pages for more info.<br>
22;; http://us.metamath.org/index.html<br>
23;; http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf<br>
24;; http://www.enm.bris.ac.uk/research/aigroup/enjl/logic/sld034.htm<br>
25;; http://www.cs.mu.oz.au/255/lec/subject-prop_resolution.pdf<br>
26;; <br><br>
27</body>
28</html>
29
30
Note: See TracBrowser for help on using the repository browser.