Comment Lab . 3

[BertLisser]

Exerc. 2

parseTest :: Form -> Bool
parseTest f = show f == (show . head . parse . show) f

is too much.

parseTest :: Form -> Bool
parseTest f = f ==  head . parse . show f

is enough.
Exerc. 4

cnfChecker (Dsj []) = False
cnfChecker (Cnj []) = False

must be

cnfChecker (Dsj []) = True
cnfChecker (Cnj []) = True

Exerc. 3

-- Testing is done by ensuring that the generated form is not in CNF. Non-CNF forms are transformed
-- into CNF. Then CNF-form is checked to make sure it actually in CNF and is logicaly equivelant to
-- the original. This test relies on the random form generator from assignment 4.
testCNFConversion :: Form -> Bool
testCNFConversion f = (not (isCNFConjunction f)) --> isCNFConjunction f' && equiv f f'
                    where
                        f' = cnf f

can be replace by the stronger

-- Testing is done by ensuring that the generated form is not in CNF. Non-CNF forms are transformed
-- into CNF. Then CNF-form is checked to make sure it actually in CNF and is logicaly equivelant to
-- the original. This test relies on the random form generator from assignment 4.
testCNFConversion :: Form -> Bool
testCNFConversion f =  isCNFConjunction f' && equiv f f'
                    where
                        f' = cnf f

Why can the function

convertToCNF :: Form -> Form
convertToCNF f | isLiteral f   = f
convertToCNF f | isCNFClause f = f
convertToCNF f                 = Cnj [ Dsj [ negateProp v | v <- vs ] | vs <- allVals f, not (evl vs f)]

no be simplified to

convertToCNF :: Form -> Form
convertToCNF f   = Cnj [ Dsj [ negateProp v | v <- vs ] | vs <- allVals f, not (evl vs f)]

[njtromp]

Exercise 3:

The implication is used to enforce a pre-condition. There is no need to check the conversion if the form is already in CNF.

The guards 'isLiteral' and 'isCNFClause' are there to prevent things like 'Cnj[ Dsj [1]]' which is rather unnecessary. What is the point of a conjunction or disjunction with a single literal.

[SjoerdvanderHeijden]

Regarding the comment on convertToCNF in ex.3: why rewrite something to cnf if it is already in cnf?
The "| isLiteral f" could indeed be skipped, since the isCNFClause case is there.

[BertLisser]

Keep it as simple as possible. isCNFClause consumes some extra computing time.