Patrick M patrickm7860 at yahoo.co.uk
Fri Feb 11 18:23:34 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

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
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

package time-1.1.4 ... linking ... done.