[Haskell-cafe] Haskell Help
patrickm7860 at yahoo.co.uk
Fri Feb 11 18:23:34 CET 2011
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],
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)
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-18.104.22.168 ... linking ... done.
package time-1.1.4 ... linking ... done.
Loading package random-22.214.171.124 ... linking ... done.
[[(True,"A"),(True,"B")*** Exception: Assignment.hs:(165,11)-(166,83): Non-exhaustive patterns in function rt
What should I do?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe