6252

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"LK/ex/prop: propositional examples";


11 


12 
writeln"absorptive laws of & and  ";


13 


14 
goal LK.thy " P & P <> P";


15 
by (fast_tac prop_pack 1);


16 
result();


17 


18 
goal LK.thy " P  P <> P";


19 
by (fast_tac prop_pack 1);


20 
result();


21 


22 
writeln"commutative laws of & and  ";


23 


24 
goal LK.thy " P & Q <> Q & P";


25 
by (fast_tac prop_pack 1);


26 
result();


27 


28 
goal LK.thy " P  Q <> Q  P";


29 
by (fast_tac prop_pack 1);


30 
result();


31 


32 


33 
writeln"associative laws of & and  ";


34 


35 
goal LK.thy " (P & Q) & R <> P & (Q & R)";


36 
by (fast_tac prop_pack 1);


37 
result();


38 


39 
goal LK.thy " (P  Q)  R <> P  (Q  R)";


40 
by (fast_tac prop_pack 1);


41 
result();


42 


43 
writeln"distributive laws of & and  ";


44 
goal LK.thy " (P & Q)  R <> (P  R) & (Q  R)";


45 
by (fast_tac prop_pack 1);


46 
result();


47 


48 
goal LK.thy " (P  Q) & R <> (P & R)  (Q & R)";


49 
by (fast_tac prop_pack 1);


50 
result();


51 


52 
writeln"Laws involving implication";


53 


54 
goal LK.thy " (PQ > R) <> (P>R) & (Q>R)";


55 
by (fast_tac prop_pack 1);


56 
result();


57 


58 
goal LK.thy " (P & Q > R) <> (P> (Q>R))";


59 
by (fast_tac prop_pack 1);


60 
result();


61 


62 


63 
goal LK.thy " (P > Q & R) <> (P>Q) & (P>R)";


64 
by (fast_tac prop_pack 1);


65 
result();


66 


67 


68 
writeln"Classical theorems";


69 


70 
goal LK.thy " PQ > P ~P&Q";


71 
by (fast_tac prop_pack 1);


72 
result();


73 


74 


75 
goal LK.thy " (P>Q)&(~P>R) > (P&Q  R)";


76 
by (fast_tac prop_pack 1);


77 
result();


78 


79 


80 
goal LK.thy " P&Q  ~P&R <> (P>Q)&(~P>R)";


81 
by (fast_tac prop_pack 1);


82 
result();


83 


84 


85 
goal LK.thy " (P>Q)  (P>R) <> (P > Q  R)";


86 
by (fast_tac prop_pack 1);


87 
result();


88 


89 


90 
(*If and only if*)


91 


92 
goal LK.thy " (P<>Q) <> (Q<>P)";


93 
by (fast_tac prop_pack 1);


94 
result();


95 


96 
goal LK.thy " ~ (P <> ~P)";


97 
by (fast_tac prop_pack 1);


98 
result();


99 


100 


101 
(*Sample problems from


102 
F. J. Pelletier,


103 
SeventyFive Problems for Testing Automatic Theorem Provers,


104 
J. Automated Reasoning 2 (1986), 191216.


105 
Errata, JAR 4 (1988), 236236.


106 
*)


107 


108 
(*1*)


109 
goal LK.thy " (P>Q) <> (~Q > ~P)";


110 
by (fast_tac prop_pack 1);


111 
result();


112 


113 
(*2*)


114 
goal LK.thy " ~ ~ P <> P";


115 
by (fast_tac prop_pack 1);


116 
result();


117 


118 
(*3*)


119 
goal LK.thy " ~(P>Q) > (Q>P)";


120 
by (fast_tac prop_pack 1);


121 
result();


122 


123 
(*4*)


124 
goal LK.thy " (~P>Q) <> (~Q > P)";


125 
by (fast_tac prop_pack 1);


126 
result();


127 


128 
(*5*)


129 
goal LK.thy " ((PQ)>(PR)) > (P(Q>R))";


130 
by (fast_tac prop_pack 1);


131 
result();


132 


133 
(*6*)


134 
goal LK.thy " P  ~ P";


135 
by (fast_tac prop_pack 1);


136 
result();


137 


138 
(*7*)


139 
goal LK.thy " P  ~ ~ ~ P";


140 
by (fast_tac prop_pack 1);


141 
result();


142 


143 
(*8. Peirce's law*)


144 
goal LK.thy " ((P>Q) > P) > P";


145 
by (fast_tac prop_pack 1);


146 
result();


147 


148 
(*9*)


149 
goal LK.thy " ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)";


150 
by (fast_tac prop_pack 1);


151 
result();


152 


153 
(*10*)


154 
goal LK.thy "Q>R, R>P&Q, P>(QR)  P<>Q";


155 
by (fast_tac prop_pack 1);


156 
result();


157 


158 
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)


159 
goal LK.thy " P<>P";


160 
by (fast_tac prop_pack 1);


161 
result();


162 


163 
(*12. "Dijkstra's law"*)


164 
goal LK.thy " ((P <> Q) <> R) <> (P <> (Q <> R))";


165 
by (fast_tac prop_pack 1);


166 
result();


167 


168 
(*13. Distributive law*)


169 
goal LK.thy " P  (Q & R) <> (P  Q) & (P  R)";


170 
by (fast_tac prop_pack 1);


171 
result();


172 


173 
(*14*)


174 
goal LK.thy " (P <> Q) <> ((Q  ~P) & (~QP))";


175 
by (fast_tac prop_pack 1);


176 
result();


177 


178 


179 
(*15*)


180 
goal LK.thy " (P > Q) <> (~P  Q)";


181 
by (fast_tac prop_pack 1);


182 
result();


183 


184 
(*16*)


185 
goal LK.thy " (P>Q)  (Q>P)";


186 
by (fast_tac prop_pack 1);


187 
result();


188 


189 
(*17*)


190 
goal LK.thy " ((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S))";


191 
by (fast_tac prop_pack 1);


192 
result();


193 


194 
writeln"Reached end of file.";
