1 (* Title: LK/ex/prop |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Classical sequent calculus: examples with propositional connectives |
|
7 Can be read to test the LK system. |
|
8 *) |
|
9 |
|
10 writeln"absorptive laws of & and | "; |
|
11 |
|
12 goal (theory "LK") "|- P & P <-> P"; |
|
13 by (fast_tac prop_pack 1); |
|
14 result(); |
|
15 |
|
16 goal (theory "LK") "|- P | P <-> P"; |
|
17 by (fast_tac prop_pack 1); |
|
18 result(); |
|
19 |
|
20 writeln"commutative laws of & and | "; |
|
21 |
|
22 goal (theory "LK") "|- P & Q <-> Q & P"; |
|
23 by (fast_tac prop_pack 1); |
|
24 result(); |
|
25 |
|
26 goal (theory "LK") "|- P | Q <-> Q | P"; |
|
27 by (fast_tac prop_pack 1); |
|
28 result(); |
|
29 |
|
30 |
|
31 writeln"associative laws of & and | "; |
|
32 |
|
33 goal (theory "LK") "|- (P & Q) & R <-> P & (Q & R)"; |
|
34 by (fast_tac prop_pack 1); |
|
35 result(); |
|
36 |
|
37 goal (theory "LK") "|- (P | Q) | R <-> P | (Q | R)"; |
|
38 by (fast_tac prop_pack 1); |
|
39 result(); |
|
40 |
|
41 writeln"distributive laws of & and | "; |
|
42 goal (theory "LK") "|- (P & Q) | R <-> (P | R) & (Q | R)"; |
|
43 by (fast_tac prop_pack 1); |
|
44 result(); |
|
45 |
|
46 goal (theory "LK") "|- (P | Q) & R <-> (P & R) | (Q & R)"; |
|
47 by (fast_tac prop_pack 1); |
|
48 result(); |
|
49 |
|
50 writeln"Laws involving implication"; |
|
51 |
|
52 goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"; |
|
53 by (fast_tac prop_pack 1); |
|
54 result(); |
|
55 |
|
56 goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))"; |
|
57 by (fast_tac prop_pack 1); |
|
58 result(); |
|
59 |
|
60 |
|
61 goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q) & (P-->R)"; |
|
62 by (fast_tac prop_pack 1); |
|
63 result(); |
|
64 |
|
65 |
|
66 writeln"Classical theorems"; |
|
67 |
|
68 goal (theory "LK") "|- P|Q --> P| ~P&Q"; |
|
69 by (fast_tac prop_pack 1); |
|
70 result(); |
|
71 |
|
72 |
|
73 goal (theory "LK") "|- (P-->Q)&(~P-->R) --> (P&Q | R)"; |
|
74 by (fast_tac prop_pack 1); |
|
75 result(); |
|
76 |
|
77 |
|
78 goal (theory "LK") "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)"; |
|
79 by (fast_tac prop_pack 1); |
|
80 result(); |
|
81 |
|
82 |
|
83 goal (theory "LK") "|- (P-->Q) | (P-->R) <-> (P --> Q | R)"; |
|
84 by (fast_tac prop_pack 1); |
|
85 result(); |
|
86 |
|
87 |
|
88 (*If and only if*) |
|
89 |
|
90 goal (theory "LK") "|- (P<->Q) <-> (Q<->P)"; |
|
91 by (fast_tac prop_pack 1); |
|
92 result(); |
|
93 |
|
94 goal (theory "LK") "|- ~ (P <-> ~P)"; |
|
95 by (fast_tac prop_pack 1); |
|
96 result(); |
|
97 |
|
98 |
|
99 (*Sample problems from |
|
100 F. J. Pelletier, |
|
101 Seventy-Five Problems for Testing Automatic Theorem Provers, |
|
102 J. Automated Reasoning 2 (1986), 191-216. |
|
103 Errata, JAR 4 (1988), 236-236. |
|
104 *) |
|
105 |
|
106 (*1*) |
|
107 goal (theory "LK") "|- (P-->Q) <-> (~Q --> ~P)"; |
|
108 by (fast_tac prop_pack 1); |
|
109 result(); |
|
110 |
|
111 (*2*) |
|
112 goal (theory "LK") "|- ~ ~ P <-> P"; |
|
113 by (fast_tac prop_pack 1); |
|
114 result(); |
|
115 |
|
116 (*3*) |
|
117 goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)"; |
|
118 by (fast_tac prop_pack 1); |
|
119 result(); |
|
120 |
|
121 (*4*) |
|
122 goal (theory "LK") "|- (~P-->Q) <-> (~Q --> P)"; |
|
123 by (fast_tac prop_pack 1); |
|
124 result(); |
|
125 |
|
126 (*5*) |
|
127 goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"; |
|
128 by (fast_tac prop_pack 1); |
|
129 result(); |
|
130 |
|
131 (*6*) |
|
132 goal (theory "LK") "|- P | ~ P"; |
|
133 by (fast_tac prop_pack 1); |
|
134 result(); |
|
135 |
|
136 (*7*) |
|
137 goal (theory "LK") "|- P | ~ ~ ~ P"; |
|
138 by (fast_tac prop_pack 1); |
|
139 result(); |
|
140 |
|
141 (*8. Peirce's law*) |
|
142 goal (theory "LK") "|- ((P-->Q) --> P) --> P"; |
|
143 by (fast_tac prop_pack 1); |
|
144 result(); |
|
145 |
|
146 (*9*) |
|
147 goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; |
|
148 by (fast_tac prop_pack 1); |
|
149 result(); |
|
150 |
|
151 (*10*) |
|
152 goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"; |
|
153 by (fast_tac prop_pack 1); |
|
154 result(); |
|
155 |
|
156 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
|
157 goal (theory "LK") "|- P<->P"; |
|
158 by (fast_tac prop_pack 1); |
|
159 result(); |
|
160 |
|
161 (*12. "Dijkstra's law"*) |
|
162 goal (theory "LK") "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"; |
|
163 by (fast_tac prop_pack 1); |
|
164 result(); |
|
165 |
|
166 (*13. Distributive law*) |
|
167 goal (theory "LK") "|- P | (Q & R) <-> (P | Q) & (P | R)"; |
|
168 by (fast_tac prop_pack 1); |
|
169 result(); |
|
170 |
|
171 (*14*) |
|
172 goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"; |
|
173 by (fast_tac prop_pack 1); |
|
174 result(); |
|
175 |
|
176 |
|
177 (*15*) |
|
178 goal (theory "LK") "|- (P --> Q) <-> (~P | Q)"; |
|
179 by (fast_tac prop_pack 1); |
|
180 result(); |
|
181 |
|
182 (*16*) |
|
183 goal (theory "LK") "|- (P-->Q) | (Q-->P)"; |
|
184 by (fast_tac prop_pack 1); |
|
185 result(); |
|
186 |
|
187 (*17*) |
|
188 goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"; |
|
189 by (fast_tac prop_pack 1); |
|
190 result(); |
|