90 lines
2.4 KiB
Haskell
Executable File
90 lines
2.4 KiB
Haskell
Executable File
data Prop = Const Bool
|
|
| Var Char
|
|
| Not Prop
|
|
| And Prop Prop
|
|
| Or Prop Prop
|
|
| Imply Prop Prop
|
|
| Iff Prop Prop
|
|
|
|
p1 :: Prop
|
|
p1 = And (Var 'A') (Not (Var 'A'))
|
|
|
|
p2 :: Prop
|
|
p2 = Imply (And (Var 'A') (Var 'B')) (Var 'A')
|
|
|
|
p3 :: Prop
|
|
p3 = Imply (Var 'A') (And (Var 'A') (Var 'B'))
|
|
|
|
p4 :: Prop
|
|
p4 = Imply (And (Var 'A') (Imply (Var 'A') (Var 'B'))) (Var 'B')
|
|
|
|
p5 :: Prop
|
|
p5 = Iff (Imply (Var 'B') (Imply (Var 'A') (Var 'C'))) (Imply (And (Var 'B') (Var 'A')) (Var 'C'))
|
|
|
|
p6 :: Prop
|
|
p6 = Iff (Or (Var 'A') (And (Var 'B') (Var 'C'))) (And (Or (Var 'A') (Var 'B')) (Or (Var 'A') (Var 'C')))
|
|
|
|
p7 :: Prop
|
|
p7 = Imply (Imply (Imply (Var 'P') (Var 'Q')) (Var 'P')) (Var 'P')
|
|
|
|
p8 :: Prop
|
|
p8 = Iff (Var 'P') (Or (Var 'P') (Var 'Q'))
|
|
|
|
p9 :: Prop
|
|
p9 = Imply (Var 'P') (Or (Var 'P') (Var 'Q'))
|
|
|
|
p10 :: Prop
|
|
p10 = Not (Imply (Imply (Var 'P') (Var 'Q')) (Imply (And (Var 'P') (Var 'R')) (And (Var 'Q') (Var 'R'))))
|
|
|
|
p11 :: Prop
|
|
p11 = Iff (And (Var 'P') (Or (Var 'Q') (Var 'R'))) (Or (And (Var 'P') (Var 'Q')) (And (Var 'P') (Var 'R')))
|
|
|
|
p12 :: Prop
|
|
p12 = Iff (Or (Not (Or (Var 'P') (Var 'Q'))) (Not (And (Var 'R') (Var 'Q')))) (Or (Not (Var 'Q')) (Not (Var 'R')))
|
|
|
|
p13 :: Prop
|
|
p13 = Iff (Iff (Var 'P') (Var 'Q')) (Or (Not (Or (Not (Var 'P')) (Not (Var 'Q')))) (Not (Or (Var 'P') (Var 'Q'))))
|
|
|
|
type Assoc k v = [(k,v)]
|
|
find :: Eq k => k -> Assoc k v -> v
|
|
find k t = head [v | (k',v) <- t, k==k']
|
|
|
|
type Sust = Assoc Char Bool
|
|
|
|
eval :: Sust -> Prop -> Bool
|
|
eval _ (Const b) = b
|
|
eval s (Var x) = find x s
|
|
eval s (Not p) = not (eval s p)
|
|
eval s (And p q) = eval s p && eval s q
|
|
eval s (Or p q) = eval s p || eval s q
|
|
eval s (Imply p q) = eval s p <= eval s q
|
|
eval s (Iff p q) = (eval s p <= eval s q) && (eval s q <= eval s p)
|
|
|
|
vars :: Prop -> [Char]
|
|
vars (Const _) = []
|
|
vars (Var x) = [x]
|
|
vars (Not p) = vars p
|
|
vars (And p q) = vars p ++ vars q
|
|
vars (Or p q) = vars p ++ vars q
|
|
vars (Imply p q) = vars p ++ vars q
|
|
vars (Iff p q) = vars p ++ vars q
|
|
|
|
bools :: Int -> [[Bool]]
|
|
bools 0 = [[]]
|
|
bools n = map (False:) bss ++ map (True:) bss
|
|
where bss = bools (n-1)
|
|
|
|
rmdumps :: Eq a => [a] -> [a]
|
|
rmdumps [] = []
|
|
rmdumps (x:xs) = x : filter (/= x) (rmdumps xs)
|
|
|
|
susts :: Prop -> [Sust]
|
|
susts p = map (zip vs) (bools (length vs))
|
|
where vs = rmdumps (vars p)
|
|
|
|
esTaut :: Prop -> Bool
|
|
esTaut p = and [eval s p | s <- susts p]
|
|
|
|
esCont :: Prop -> Bool
|
|
esCont p = not (or [eval s p | s <- susts p])
|