1 (* Title: FOL/ex/prolog.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 *) |
|
6 |
|
7 Goal "app(a:b:c:Nil, d:e:Nil, ?x)"; |
|
8 by (resolve_tac [appNil,appCons] 1); |
|
9 by (resolve_tac [appNil,appCons] 1); |
|
10 by (resolve_tac [appNil,appCons] 1); |
|
11 by (resolve_tac [appNil,appCons] 1); |
|
12 prth (result()); |
|
13 |
|
14 Goal "app(?x, c:d:Nil, a:b:c:d:Nil)"; |
|
15 by (REPEAT (resolve_tac [appNil,appCons] 1)); |
|
16 result(); |
|
17 |
|
18 |
|
19 Goal "app(?x, ?y, a:b:c:d:Nil)"; |
|
20 by (REPEAT (resolve_tac [appNil,appCons] 1)); |
|
21 back(); |
|
22 back(); |
|
23 back(); |
|
24 back(); |
|
25 result(); |
|
26 |
|
27 |
|
28 (*app([x1,...,xn], y, ?z) requires (n+1) inferences*) |
|
29 (*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*) |
|
30 |
|
31 Goal "rev(a:b:c:d:Nil, ?x)"; |
|
32 val rules = [appNil,appCons,revNil,revCons]; |
|
33 by (REPEAT (resolve_tac rules 1)); |
|
34 result(); |
|
35 |
|
36 Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; |
|
37 by (REPEAT (resolve_tac rules 1)); |
|
38 result(); |
|
39 |
|
40 Goal "rev(?x, a:b:c:Nil)"; |
|
41 by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*) |
|
42 back(); |
|
43 back(); |
|
44 |
|
45 (*backtracking version*) |
|
46 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1); |
|
47 |
|
48 choplev 0; |
|
49 by prolog_tac; |
|
50 result(); |
|
51 |
|
52 Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; |
|
53 by prolog_tac; |
|
54 result(); |
|
55 |
|
56 (*rev([a..p], ?w) requires 153 inferences *) |
|
57 Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"; |
|
58 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); |
|
59 (*Poly/ML: 4 secs >> 38 lips*) |
|
60 result(); |
|
61 |
|
62 (*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences; |
|
63 total inferences = 2 + 1 + 17 + 561 = 581*) |
|
64 Goal |
|
65 "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"; |
|
66 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); |
|
67 (*Poly/ML: 29 secs >> 20 lips*) |
|
68 result(); |
|