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.