-
Notifications
You must be signed in to change notification settings - Fork 0
/
propositional.hs
81 lines (63 loc) · 2.3 KB
/
propositional.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
{-# LANGUAGE UnicodeSyntax #-}
module Propositional where
import Data.List(nub)
----------------------------------------
----------------------------------------
data Formula = Var String
| Not Formula
| Formula :& Formula
| Formula :| Formula
| Formula :=> Formula
| Formula :<=> Formula
deriving (Ord, Eq)
instance Show Formula where
show (Var v) = show v
show (Not p) = "¬" ++ show p
show (p :& q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
show (p :| q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"
show (p :=> q) = "(" ++ show p ++ " → " ++ show q ++ ")"
show (p :<=> q) = "(" ++ show p ++ " ⟷ " ++ show q ++ ")"
type Literal = Formula
type Clausula = [Literal]
infixl 9 :&
infixl 9 :|
infixr 7 :=>
infixl 8 :<=>
----------------------------------------
----------------------------------------
-- Transform a formula p into Negative Normal Form
fnn :: Formula -> Formula
fnn expr@(Var _) = expr
fnn expr@(Not (Var _)) = expr
fnn (Not (Not expr)) = expr
fnn (exp1 :& exp2) = fnn exp1 :& fnn exp2
fnn (Not (exp1 :& exp2)) = fnn $ Not exp1 :| Not exp2
fnn (exp1 :| exp2) = fnn exp1 :| fnn exp2
fnn (Not (exp1 :| exp2)) = fnn $ Not exp1 :& Not exp2
fnn (exp1 :=> exp2) = fnn $ Not exp1 :| exp2
fnn (Not (exp1 :=> exp2)) = fnn $ exp1 :& Not exp2
fnn (exp1 :<=> exp2)
= let a = exp1 :& exp2
b = Not exp1 :& Not exp2
in fnn $ a :| b
fnn (Not (exp1 :<=> exp2))
= let a = exp1 :| exp2
b = Not exp1 :| Not exp2
in fnn $ a :& b
-- Transform a formula p into Conjunctive Normal Form
fnc :: Formula -> Formula
fnc = fnc' . fnn
where fnc' :: Formula -> Formula
fnc' (exp1 :& exp2) = fnc' exp1 :& fnc' exp2
fnc' (exp1 :| exp2) = fnc' exp1 `dist` fnc' exp2
fnc' expr = expr
dist :: Formula -> Formula -> Formula
dist (e11 :& e12) e2 = (dist e11 e2) :& (dist e12 e2)
dist e1 (e21 :& e22) = (dist e1 e21) :& (dist e1 e22)
dist e1 e2 = e1 :| e2
-- Given a formula returns the list of variables that compose it.
variables :: Formula -> Clausula
variables var@(Var _) = [var]
variables (Not x) = variables x
variables (p :| q) = nub $ variables p ++ variables q
variables (p :& q) = nub $ variables p ++ variables q