[Haskell-cafe] Haskell Help

[Daniel Fischer]

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.