I need to write two functions for a coursework that will behave as follows... unction 1)removeTautologies :: Formula->Formula If in a clause, a literal and its negation are found, it means that the clause will be true, regardless of the value finally assigned to that propositional variable. Consider the following example: (A v B v -A) ^ (B v C v A) The first clause contains the literals A and -A. This means that the clause will always be true, in which case it can be simplify the whole set to simply (B v C v A) . I was tinking of using something like removeTautologies (f:fs)=filter rTf:removeTautologies fs where rT-is supposed to take the firs Literal from the clasue and search for a similar one,if one si found we compare the values if not the we go to the second literal. ->Function 2)pureLiteralDeletion :: Formula->Formula This is a little bit complicate but from What I get this function is suppose to implement a simplification step that assumes as true any atom in a formula that appears exclusively in a positive or negative form (not both). Consider the formula: (P v Q v R) ^ (P v Q v -R) ^ (-Q v R) Note that in this formula P is present but -P is not. Using Pure Literal Deletion it can be assumed that the value of P will be True thus simplifying the formula to (-Q v R). If the literal were false then the literal would simply be deleted from the clauses it appears in. In that case any satisfying model for the resulting formula would also be a satisfying model for the formula when we assume that the literal is true. removeTautologies :: Formula -> Formula removeTautologies = map rt.map head.group.sort where rt ((x, x') : (y, y') : rest) | x' == y' = rt rest | otherwise = (x, x') : rt ((y, y') : rest) pureLiteralDeletion :: Formula -> Formula pureLiteralDeletion = map lD.map head.group.sort.concat where lD ((x, x') : (y, y') : rest) | x' == y' && x/=y = lD rest | otherwise = (x, x') : lD ((y, y') : rest) this is what I've witten so far but they don't wok poperly....any sugestions?