blob: 844e867f67bab1084d34f01a0824b45f190c39b7 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
%%%
%%% NAME/LOGIN-ID _____________________/______________________
%%%
%%% ACKNOWLEDGMENTS:
%%% * List the names of people whom you worked with or who helped you
%%% with this assignment
%%% * Cite any references you used to complete this work
%%%
%%% ===================
%%% Propositional Logic
%%% ===================
%%%
%%% Prove these theorems using only the (SPLIT) and (FLATTEN) commands
%%% ~~~~
th_A: Theory
BEGIN
%%% Elementary propositions.
%%%
p,q,r: bool
%%%
%%% Propositional Formulas
%%%
%%% (CLAIM, CONJECTURE, ..., THEOREM all mean the same thing)
%%%
A_0: CLAIM ((p => q) AND p) => q
A_1: CONJECTURE ((p AND q) AND r) => (p AND (q AND r))
A_2: COROLLARY NOT (p OR q) IFF (NOT p AND NOT q)
A_3: FACT NOT (p AND q) IFF (NOT p OR NOT q)
A_4: FORMULA (p => (q => r)) IFF (p AND q => r)
A_5: LAW (p AND (q OR r)) IFF (p AND q) OR (p AND r)
A_6: LEMMA (p OR (q AND r)) IFF (p OR q) AND (p OR r)
A_7: PROPOSITION ((p => q) AND (p => r)) IFF (p => (q AND r))
A_8: SUBLEMMA ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p))
A_9: THEOREM ((p OR q) AND r) => (p AND (q AND r))
A_10: CLAIM p => (q => p)
A_11: CLAIM ((p => (q => r)) => ((p => q) => (p => r)))
A_12: CLAIM ((NOT q) => (NOT p)) => (((NOT q) => p) => q)
END th_A
|
