Part (a): A type!
—————–
For this part, you should define a datatype to represent logical formulae
(F or G). Your datatype should (somehow) incorporate the following cases:
Syntax | Meaning
———+————————————————
P, Q, R | Propositional variable (any string)
¬ F | Negation of F (where F is any formula)
F ∧ G | Conjunction of F and G
F ∨ G | Disjunction of F and G
——————————————————————————-}
data Formula = — Your definition goes here
deriving (Eq, Show)
— Constructor functions
variable :: String -> Formula
variable = undefined
neg :: Formula -> Formula
neg = undefined
conj, disj :: Formula -> Formula -> Formula
conj = undefined
disj = undefined
— A few examples.
form1, form2, form3 :: Formula
form1 = neg (variable “X”)
form2 = (neg (variable “X”) `conj` variable “Y”) `disj` variable “Z”
form3 = (variable “X” `disj` variable “Y”) `conj` variable “Z”
{——————————————————————————-
Part (b): A function!
———————
For this part, you should write a function that converts an arbitrary formula
into negation normal form. A formula is in negation normal form (NNF) if the
negation operator is ONLY applied to propositional variables, not to any other
type of formula. For example:
Formula | Negation normal form
————-+———————
¬(P ∧ ¬Q) | ¬P ∨ Q
¬(¬P ∨ ¬Q) | P ∧ Q
How should you convert a formula into NNF? You’ll need three logical
equivalences:
¬¬P ≡ P
¬(F ∨ G) ≡ ¬F ∧ ¬G
¬(F ∧ G) ≡ ¬F ∨ ¬G
Keep in mind you may have to apply these rules multiple times. For example,
given the formula
¬(P ∧ ¬P)
you could apply the third rule (one of de Morgan’s laws) to get
¬P ∨ ¬(¬P)
but this isn’t yet in NNF! You then have to apply the first rule
(double-negation elimination) to get
¬P ∨ P
——————————————————————————-}
nnf :: Formula -> Formula
nnf = undefined — Your implementation goes here