That look compicated....I have a couple of functions at my disposal remove :: (Eq a) )a ->[a] ->[a] -This function removes an item from a list. neg :: Literal->Literal -This function flips a literal (ie. from P to :P and from :P to P). falseClause :: Model -> Clause -> Bool -This function takes a Model and a Clause and returns True if the clause is unsatisfied by the model or False otherwise. falseClauses :: Formula -> Model -> [Clause] -This function takes a Formula and a Model and returns the list of clauses of the formula that are not satisfied. assignModel :: Model -> Formula -> Formula -This function applies the assign function for all the assignments of a given model. checkFormula :: Formula -> Maybe Bool This function checks whether a formula can be decided to be satisfiable or unsatisfiable based on the effects of the assign function. satisfies :: Model -> Formula -. Bool This function checks whether a model satisfies a formula. This is done with the combination of the assignModel and checkFormula functions. I was thinking something similair with this resFormula :: Formula -> Literal -> Formula resFormula f literal = let f' = filter (literal `notElem`) f in -- Get rid of satisfied clauses map (filter (/= (neg literal))) f' -- Remove negations from clauses But I can't match the expected type....also I have to choose an atom.. -- View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3385699.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.