-
Notifications
You must be signed in to change notification settings - Fork 1
/
Formulas_en.hs
134 lines (100 loc) · 3.24 KB
/
Formulas_en.hs
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
module Formulas (module Formulas) where
{- We define the data type "Formula", which reflects the writing of the formulas in Polish form. Atomic formulas are based on integers (Int). -}
data Formula = Fa Int
| C Formula Formula
| E Formula Formula
| K Formula Formula
| N Formula
| A Formula Formula
deriving (Eq, Ord)
{-
Various formulas for testing
-}
u10 = K (Fa 10)(Fa 11)
u9 = K (Fa 9) u10
u8 = K (Fa 8) u9
u7 = K (Fa 7) u8
u6 = K (Fa 6) u7
u5 = K u6 (Fa 5)
u4 = K (Fa 4) u5
u3 = K (Fa 3) u4
u2 = K (Fa 2) u3
u1 = K (Fa 1) u2
x1=E (Fa 1) (Fa 2) :: Formula -- x1 = p1 <-> p2
x2=K (Fa 2) (Fa 1) :: Formula -- x2 = p2 ^ p1
x3=C (Fa 1) (Fa 2) :: Formula -- x3 = p1 -> p2
x4=N x3 :: Formula -- ¬(p1 -> p2)
x5=A x4 x2 :: Formula -- ¬(p1 -> p2) v (p1 <-> p2)
x6=N x5 :: Formula -- ¬(¬(p1 -> p2) v (p1 <-> p2))
x7=N x1 :: Formula -- ¬(p1 <-> p2)
x=A x6 x7 :: Formula -- ¬(¬(p1 -> p2) v (p1 <-> p2)) v ¬(p1 <-> p2)
{-
y1 = se x
y2 = sc y1
y3 = ing y2
y4 = dak y3
y5 = dak y4
y6 = aa y5
y7 = aa y6
-}
z2 = K (Fa 1) (Fa 2)
z3 = K (Fa 3) z2
z4 = K (Fa 4) z3
z5 = K (Fa 5) z4
z6 = K (Fa 6) z5
z7 = K (Fa 7) z6
z8 = K (Fa 8) z7
z9 = K (Fa 9) z8
z10= K (Fa 10) z9
z11= K (Fa 11) z10
z12= K (Fa 12) z11
z13= K (Fa 13) z12
z14= K (Fa 14) z13
z15= K (Fa 15) z14
z16= K (Fa 16) z15
z17= K (Fa 17) z16
z18= K (Fa 18) z17
{- Create a formula consisting only of conjunctions -}
f :: Int -> Int -> Formula
f 0 n = K (Fa n) (N (Fa n))
f m n = K (f (m -1) n) (f (m-1) (n+2^m))
{- Some examples of tautologies -}
taut1::Formula
taut2::Formula
taut3::Formula
taut31::Formula
taut32::Formula
taut33::Formula
taut4::Formula
taut41::Formula
taut42::Formula
taut43::Formula
modponen::Formula
modtol::Formula
peirce::Formula
silogismo1::Formula
silogismo2::Formula
taut1 = C (C (Fa 1) (C (Fa 2) (Fa 3))) (C (C (Fa 1) (Fa 2)) (C (Fa 1) (Fa 3)))
-- (p -> (q -> r))-> ((p -> q) -> (p -> r))
taut2 = C (C (C (C (Fa 1) (Fa 2)) (Fa 2)) (C (Fa 3) (Fa 2))) (C (Fa 1) (C (Fa 3) (Fa 2)))
-- (((p -> q) -> q) -> (r -> q)) -> (p -> (r -> q))
taut3 = C (C (C (C (C (Fa 1) (Fa 2)) (C (N (Fa 3)) (N (Fa 4)))) (Fa 3)) (Fa 5)) (C (C (Fa 5) (Fa 1)) (C (Fa 4) (Fa 1)))
taut31 = C (C (C (C (Fa 1) (Fa 2)) (C (N (Fa 3)) (N (Fa 4)))) (Fa 3)) (Fa 5)
-- (((p -> q) -> (¬r -> ¬s)) -> r) -> t
taut32 = C (Fa 5) (Fa 1) -- t -> p
taut33 = C (Fa 4) (Fa 1) -- s -> p
taut41 = C (C (Fa 1) (Fa 2)) (Fa 3)
taut42 = C (Fa 2) (C (Fa 3) (Fa 5))
taut43 = C (Fa 2) (Fa 5)
taut4 = C (taut41) (C (Fa 4) (C (taut42) (taut43)))
-- taut3 = (taut31 -> (taut32 -> taut33))
modponen = C (K (Fa 1) (C (Fa 1) (Fa 2))) (Fa 2)
-- (p ^ (p -> q)) -> q
modtol = C (K (C (Fa 1) (Fa 2)) (N (Fa 2))) (N (Fa 1))
-- ((p -> q) ^ ¬q) -> ¬p
peirce = C (C (C (Fa 1) (Fa 2)) (Fa 1)) (Fa 1)
-- ((p -> q) -> p) -> p
silogismo1 = C (C (Fa 1) (Fa 2)) (C (C (Fa 2) (Fa 3)) (C (Fa 1) (Fa 3)))
-- (p -> q) -> ((q -> r) -> (p -> r))
silogismo2 = C (C (Fa 2) (Fa 3)) (C (C (Fa 1) (Fa 2)) (C (Fa 1) (Fa 3)))
-- (q -> r) -> ((p -> q) -> (p -> r))