[Haskell-cafe] Haskell Help
patrickm7860 at yahoo.co.uk
Fri Feb 11 18:25:24 CET 2011
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.
module Algorithm where
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
Loading package old-locale-188.8.131.52 ... linking ... done.
Loading package time-1.1.4 ... linking ... done.
Loading package random-184.108.40.206 ... linking ... done.
[[(True,"A"),(True,"B")*** Exception: Assignment.hs:(165,11)-(166,83):
Non-exhaustive patterns in function rt
What should I do?
View this message in context: http://haskell.1045720.n5.nabble.com/Haskell-Help-tp3381647p3381647.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
More information about the Haskell-Cafe