Comment 3

[BertLisser]

cnf :: Form -> Form
cnf = flat . cnf' . nnf . arrowfree
    where cnf' :: Form -> Form
          cnf' (Cnj [f1,f2])       = Cnj [cnf' f1, cnf' f2]
          cnf' (Dsj [f1,f2])       = dist (head [cnf' f1, cnf' f2]) ([cnf' f1, cnf' f2] !! 1) 
          cnf' expr                = expr

          dist (Cnj [e11, e12]) e2 = Cnj [e11 `dist` e2, e12 `dist` e2] 
          dist e1 (Cnj [e21,e22])  = Cnj [e1 `dist` e21, e1 `dist` e22]
          dist e1 e2               = Dsj [e1,e2]

Too restricted. 'Cnj' and 'Dsj' can have a number of arguments unequal to 2. 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]

The same remark for

substituteLiterals :: Int -> Form -> Form
substituteLiterals 0 (Prop n) = Dsj [Prop n, Prop (n + 1)]
substituteLiterals 1 (Prop n) = Cnj [Prop n, Prop (n + 1)]
substituteLiterals 2 (Prop n) = Impl (Prop n) (Prop (n + 1))
substituteLiterals 3 (Prop n) = Equiv (Prop n) (Prop (n + 1))
substituteLiterals 4 (Prop n) = Neg (Prop n)
substituteLiterals 5 (Prop n) = Prop n

[p-kostic]

For the first two, this is something I glanced over because all the forms for the test cases I made and those that were included did not have more than 2 literals. My apologies!

I should have noticed since the last step of the pipeline ('flat') does account for such cases. Because you basically had to account for it there.