tautology_checker.hs

import Data.List
data Prop = Const Bool
            | Var Char
            | Not Prop
            | And Prop Prop
            | Imply Prop Prop


p1 :: Prop
p1 = And (Var 'A') (Not( Var 'A'))

p2 :: Prop
p2 = Imply(And (Var 'A') (Var 'B')) (Var 'A')

p3 :: Prop
p3 = Imply(Var 'A') (And (Var 'A') (Var 'B'))

p4 :: Prop
p4 = Imply(And (Var 'A') (Imply (Var 'A') (Var 'B'))) (Var 'B')

type Assoc k v = [(k,v)]
type Subst = Assoc Char Bool

eval :: Subst -> Prop -> Bool
eval _ (Const b) = b
eval s (Var x) = find x s
eval s (Not p) = not (eval s p)
eval s (And p q) = eval s p && eval s q
eval s (Imply p q) = eval s p <= eval s q