On Friday 11 February 2011 18:25:24, PatrickM wrote: > I'm writting a function that will remove tautologies from a fomula.The > basic idea is that 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.My appoach is to create a > function that will remove this but for a clause and map it to the > fomula.Of course I have to remove duplicates at the beginning.
Tip: write a function isTautology :: Clause -> Bool for that, the function partition from Data.List might be useful. Then removeTautologies becomes a simple filter. > > module Algorithm where > > import System.Random > import Data.Maybe > import Data.List > > type Atom = String > type Literal = (Bool,Atom) > type Clause = [Literal] > type Formula = [Clause] > type Model = [(Atom, Bool)] > type Node = (Formula, ([Atom], Model)) > removeTautologies :: Formula -> Formula > removeTautologies = map tC.map head.group.sort > where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest > > | otherwise = (vx, x) : rt > | ((vy, > > y) : clauses) > Now I have problems when I try to give it a formula (for example (A v B > v -A) ^ (B v C v A)).Considering that example 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) . > But I get the following > > Loading package old-locale-1.0.0.2 ... linking ... done. > Loading package time-1.1.4 ... linking ... done. > Loading package random-1.0.0.2 ... linking ... done. > [[(True,"A"),(True,"B")*** Exception: > Assignment.hs:(165,11)-(166,83): Non-exhaustive patterns in function rt > > What should I do? You have to treat the cases of lists with zero or one entries in rt. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
