Removing a Tautology in Haskell

I'm writting a function that will remove tautologies from a fomula,the problem is that is working only for consecutive duplicates.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 an开发者_高级运维d 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
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 because I'm only checking for consecutive literals and I do not know how to change that since I'm new to haskell(not an excuse,I know),so when I try to give it a formula (for example (A v B v -A) ^ (B v C v A)) it just returns the exact input.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) .

What changes should I write for my function so that I can remove a tautology in the right way? Can I implement sortBy?If yes ,how?map head.group.sortBy snd?

---

Try this: Make a [structure of your choice] of the elements

1. If the element is inside the structure, remove it from the list.
2. Elseway, pass it both to the outout list and add it to your structure.

This is basically the same as nubBy, find out how to implement it!