Comment lab 3

[BertLisser]

Exerc. 1

-- Testing below.
testContradiction :: IO Bool
testContradiction = do
    x <- generateForm
    let simplifiedX = (contradiction (nnf (arrowfree x)))
    if (contradiction x)
        then return ((not (satisfiable x)) && simplifiedX)
        else return (not simplifiedX)

is wrong for

x = Impl((Prop 1) (Prop2)

This is no contradiction and returns True (because of not simplified(X))
Exerc. 2

testParser :: String -> Bool
testParser x = length (filter (/= ' ') (show (parse x))) == (elementsIn x)
    where
        elementsIn s = 2 + length (filter (/= ' ') s)

That is too restricted. Testing only the length of a string.

Exerc. 3

-- A precondition for the running of cnf is that it must be arrowfree as produced
-- by the arrowfree function. The function matches patters of logic and converts
-- them going inward. Should be ran iteratively to convert it to the right
-- form bit by bit (We did this with help of Pieter Donkers). 
cnf :: Form -> Form
cnf (Prop x) = Prop x
cnf (Neg f) = Neg (cnf f)
cnf (Dsj [Cnj [x,y],z]) = Cnj [cnf (Dsj [z,x]), cnf (Dsj [z,y])]
cnf (Cnj [z, Cnj [x, y]]) = Cnj [cnf (Dsj [z,x]), cnf (Dsj [z,y])]
cnf (Cnj fs) = Dsj (map cnf fs)
cnf (Dsj fs) = Dsj (map cnf fs)

You are half way.
Here a solution.

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]