PROBLEM 3 (Regular): Disjunctive normal form (DNF) refers to a form of Boolean formulae which is in negation normal form and in which no disjunction appears inside a conjunction. For example, this formula is in DNF: A \/ (B /\ C) \/ (B /\ ~D) while this formula is not: A \/ (B /\ (C \/ D)) nor is this one: A \/ (B /\ ~(C /\ D)) Your third task is to write a function `dnf` which transforms input Boolean formulae *in NNF* into Boolean formulae in DNF. Your implementation will need the following equations (A,B, and C are arbitrary formulae) Distribution of /\ over \/: A /\ (B \/ C) == (A /\ B) \/ (A /\ C) (A \/ B) /\ C == (A /\ C) \/ (B /\ C) You do not need to perform other simplifications (such as reducing A /\ A to A or reducing A \/ ~A to True). For testing, I have provided a function `isDnf`, which returns `True` if its input is in disjunctive normal form and `False` otherwise. You should NOT use the `isDnf` function in your implementation of `dnf`. -------------------------------------------------------------------------------} dnf :: Formula -> Formula dnf = error "dnf not implemented" isDnf phi = isDnf' 0 phi where isDnf' _ (Var x) = True isDnf' _ (Not (Var x)) = True isDnf' 0 (Or phi psi) = isDnf' 0 phi && isDnf' 0 psi isDnf' 0 (And phi psi) = isDnf' 1 phi && isDnf' 1 psi isDnf' 1 (And phi psi) = isDnf' 1 phi && isDnf' 1 psi isDnf' _ _ = False dnfTests = TestList [ "right distribution" ~: isDnf (dnf (And (Var "A") (Or (Var "B") (Var "C")))) ~?= True , "left distribution" ~: isDnf (dnf (And (Or (Var "A") (Var "B")) (Var "C"))) ~?= True -- Your tests go here ]