summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Sequents/LK/prop.ML

author | wenzelm |

Sun Sep 18 15:20:08 2005 +0200 (2005-09-18) | |

changeset 17481 | 75166ebb619b |

parent 6252 | 935f183bf406 |

permissions | -rw-r--r-- |

converted to Isar theory format;

1 (* Title: LK/ex/prop

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1992 University of Cambridge

6 Classical sequent calculus: examples with propositional connectives

7 Can be read to test the LK system.

8 *)

10 writeln"absorptive laws of & and | ";

12 goal (theory "LK") "|- P & P <-> P";

13 by (fast_tac prop_pack 1);

14 result();

16 goal (theory "LK") "|- P | P <-> P";

17 by (fast_tac prop_pack 1);

18 result();

20 writeln"commutative laws of & and | ";

22 goal (theory "LK") "|- P & Q <-> Q & P";

23 by (fast_tac prop_pack 1);

24 result();

26 goal (theory "LK") "|- P | Q <-> Q | P";

27 by (fast_tac prop_pack 1);

28 result();

31 writeln"associative laws of & and | ";

33 goal (theory "LK") "|- (P & Q) & R <-> P & (Q & R)";

34 by (fast_tac prop_pack 1);

35 result();

37 goal (theory "LK") "|- (P | Q) | R <-> P | (Q | R)";

38 by (fast_tac prop_pack 1);

39 result();

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();

46 goal (theory "LK") "|- (P | Q) & R <-> (P & R) | (Q & R)";

47 by (fast_tac prop_pack 1);

48 result();

50 writeln"Laws involving implication";

52 goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";

53 by (fast_tac prop_pack 1);

54 result();

56 goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";

57 by (fast_tac prop_pack 1);

58 result();

61 goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q) & (P-->R)";

62 by (fast_tac prop_pack 1);

63 result();

66 writeln"Classical theorems";

68 goal (theory "LK") "|- P|Q --> P| ~P&Q";

69 by (fast_tac prop_pack 1);

70 result();

73 goal (theory "LK") "|- (P-->Q)&(~P-->R) --> (P&Q | R)";

74 by (fast_tac prop_pack 1);

75 result();

78 goal (theory "LK") "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)";

79 by (fast_tac prop_pack 1);

80 result();

83 goal (theory "LK") "|- (P-->Q) | (P-->R) <-> (P --> Q | R)";

84 by (fast_tac prop_pack 1);

85 result();

88 (*If and only if*)

90 goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";

91 by (fast_tac prop_pack 1);

92 result();

94 goal (theory "LK") "|- ~ (P <-> ~P)";

95 by (fast_tac prop_pack 1);

96 result();

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 *)

106 (*1*)

107 goal (theory "LK") "|- (P-->Q) <-> (~Q --> ~P)";

108 by (fast_tac prop_pack 1);

109 result();

111 (*2*)

112 goal (theory "LK") "|- ~ ~ P <-> P";

113 by (fast_tac prop_pack 1);

114 result();

116 (*3*)

117 goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";

118 by (fast_tac prop_pack 1);

119 result();

121 (*4*)

122 goal (theory "LK") "|- (~P-->Q) <-> (~Q --> P)";

123 by (fast_tac prop_pack 1);

124 result();

126 (*5*)

127 goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";

128 by (fast_tac prop_pack 1);

129 result();

131 (*6*)

132 goal (theory "LK") "|- P | ~ P";

133 by (fast_tac prop_pack 1);

134 result();

136 (*7*)

137 goal (theory "LK") "|- P | ~ ~ ~ P";

138 by (fast_tac prop_pack 1);

139 result();

141 (*8. Peirce's law*)

142 goal (theory "LK") "|- ((P-->Q) --> P) --> P";

143 by (fast_tac prop_pack 1);

144 result();

146 (*9*)

147 goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";

148 by (fast_tac prop_pack 1);

149 result();

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();

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

157 goal (theory "LK") "|- P<->P";

158 by (fast_tac prop_pack 1);

159 result();

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

162 goal (theory "LK") "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))";

163 by (fast_tac prop_pack 1);

164 result();

166 (*13. Distributive law*)

167 goal (theory "LK") "|- P | (Q & R) <-> (P | Q) & (P | R)";

168 by (fast_tac prop_pack 1);

169 result();

171 (*14*)

172 goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";

173 by (fast_tac prop_pack 1);

174 result();

177 (*15*)

178 goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";

179 by (fast_tac prop_pack 1);

180 result();

182 (*16*)

183 goal (theory "LK") "|- (P-->Q) | (Q-->P)";

184 by (fast_tac prop_pack 1);

185 result();

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();