Comment

[BertLisser]

exercise1 = do
    putStrLn "Exercise 1:"
    putStr "prop_Contradiction "
    putStr " >  "
    quickCheck prop_Contradiction
    putStr "prop_Tautology     "
    putStr " >  "
    quickCheck prop_Tautology
    putStr "prop_Equiv         "
    putStr " >  "
    quickCheck prop_Equiv
    putStr "prop_Entails       "
    putStr " >  "
    quickCheck prop_Entails
    putStrLn ""

This test only the occurrences of false positives because the chance that quickcheck generates of a contradiction is very low.

Too complicated. Why not directly a definition of cnf without help of toCnf,

cnf :: Form -> Form
cnf = fromClauses . toCnf

toCnf :: Form -> Clauses
toCnf = toCnfClauses . nnf . arrowfree

Why not

cnf :: Form -> Form
cnf x = cnf' $ nnf $ arrowfree x

-- preconditions: input is arrowfree and in nnf
cnf' :: Form -> Form
cnf' (Prop x) = Prop x
cnf' (Neg (Prop x)) = Neg (Prop x)
cnf' (Cnj fs) = Cnj (map cnf' fs)
cnf' (Dsj []) = Dsj []
cnf' (Dsj [f]) = cnf' f
cnf' (Dsj (f1:f2:fs)) = dist (cnf' f1) (cnf' (Dsj(f2:fs)))

dist :: Form -> Form -> Form
dist (Cnj []) f = Cnj[] {-- f --}
dist (Cnj [f1]) f2 = dist f1 f2
dist (Cnj (f1:fs)) f2 = Cnj [dist f1 f2, dist (Cnj fs) f2]
dist f (Cnj []) = Cnj[] {-- f --}
dist f1 (Cnj [f2]) = dist f1 f2
dist f1 (Cnj (f2:fs)) = Cnj [dist f1 f2, dist f1 (Cnj fs)]
dist f1 f2 = Dsj [f1,f2]

?

Exercise 4

genList :: Int -> Int -> Gen [Form]
            genList nprop size = do
                w <- choose (2, size)
                sequence $ [genForm nprop (size `quot` w) | _ <- [1..w]]

Too restricted. Must become

w <- choose (0, size)