data BE vn
= F
| T
| Var vn
| Not (BE vn)
| And (BE vn) (BE vn)
| Or (BE vn) (BE vn)
| Imp (BE vn) (BE vn)
| Eqv (BE vn) (BE vn)
deriving (Eq, Read, Show)
type BE1 = BE Int
type Literal vn = (vn,Bool)
type Conjunction vn = [Literal vn]
type Disjunction vn = [Conjunction vn]
pos :: (Ord vn) => BE vn -> Disjunction vn
pos F = []
pos T = [[]]
pos (Var n) = [[(n,True)]]
pos (Not e) = neg e
pos (And e f) = prune (mk_and (pos e) (pos f))
pos (Or e f) = prune (mk_or (pos e) (pos f))
pos (Imp e f) = prune (mk_or (neg e) (pos f)) -- pos (Or (Not e) f)
pos (Eqv e f) = pos (Or (And e f) (And (Not e) (Not f)))
neg :: (Ord vn) => BE vn -> Disjunction vn
neg F = [[]]
neg T = []
neg (Var n) = [[(n,False)]]
neg (Not e) = pos e
neg (And e f) = prune (mk_or (neg e) (neg f))
neg (Or e f) = prune (mk_and (neg e) (neg f))
neg (Imp e f) = prune (mk_and (pos e) (neg f))
neg (Eqv e f) = neg (Or (And e f) (And (Not e) (Not f)))
prune :: Ord vn => Disjunction vn -> Disjunction vn
prune d = [c | c <- d, not(or [subsumes c1 c | c1 <- d])]
subsumes :: Ord vn => Conjunction vn -> Conjunction vn -> Bool
subsumes a@(x@(u,f):xs) b@(y@(v,g):ys) =
case compare u v of
LT -> False
GT -> subsumes a ys
EQ -> f == g && subsumes xs ys
subsumes (_:_) [] = False
subsumes [] (_:_) = True
subsumes [] [] = False
mk_or :: Ord vn => Disjunction vn -> Disjunction vn -> Disjunction vn
mk_or a@(x:xs) b@(y:ys) =
case c_compare x y of
LT -> x : mk_or xs b
GT -> y : mk_or a ys
EQ -> x : mk_or xs ys
mk_or a@(_:_) [] = a
mk_or [] b = b
c_compare :: Ord vn => Conjunction vn -> Conjunction vn -> Ordering
c_compare ((u,f):xs) ((v,g):ys) =
case compare u v of
LT -> LT
GT -> GT
EQ -> case compare f g of
LT -> LT
GT -> GT
EQ -> c_compare xs ys
c_compare (_:_) [] = GT
c_compare [] (_:_) = LT
c_compare [] [] = EQ
mk_and :: Ord vn => Disjunction vn -> Disjunction vn -> Disjunction vn
mk_and d1 d2 = [fromJust c
| c1 <- d1, c2 <- d2, let c = merge c1 c2, isJust c ]
isJust (Just _ ) = True
isJust (Nothing) = False
fromJust (Just x ) = x
fromJust (Nothing) = error "fromJust Nothing"
merge :: Ord vn => Conjunction vn -> Conjunction vn -> Maybe (Conjunction vn)
merge a@(x@(u,f):xs) b@(y@(v,g):ys) =
case compare u v of
LT -> case merge xs b of { Nothing -> Nothing; Just r -> Just (x:r) }
GT -> case merge a ys of { Nothing -> Nothing; Just r -> Just (y:r) }
EQ -> if f == g then
case merge xs ys of { Nothing -> Nothing; Just r -> Just (x:r) }
else Nothing
merge a@(_:_) [] = Just a
merge [] b = Just b
shows_lit :: Literal Int -> String -> String
shows_lit (v,True) s = shows v s
shows_lit (v,False) s = '~' : shows v s
shows_con :: Conjunction Int -> String -> String
shows_con [] s = "{}" ++ s
shows_con (x:xs) s = '{' : shows_lit x (shows_con_tail xs s)
where shows_con_tail [] s = '}' : s
shows_con_tail (x:xs) s = ',' : shows_lit x (shows_con_tail xs s)
shows_dis :: Disjunction Int -> String -> String
shows_dis [] s = "{}" ++ s
shows_dis (x:xs) s = '{' : shows_con x (shows_dis_tail xs s)
where shows_dis_tail [] s = '}' : s
shows_dis_tail (x:xs) s = ',' : shows_con x (shows_dis_tail xs s)
t :: Int -> String
t n = shows_dis (pos (tc n)) ""
{- Here are some test cases -}
tc :: Int -> BE1
tc 1 = (Var 1)
tc 2 = (Or (Var 1) (Var 1))
tc 3 = (Eqv (Imp (Var 1) (Var 2)) (Or (Not (Var 1)) (Var 2)))
tc 4 = (Eqv (And (Var 1) (Var 1)) (Var 1))
tc 5 = (And (And (And (Eqv (Var 13) (Or (And F (Var 1)) (Or (And F (Var
5)) (And (Var 1) (Var 5))))) (Eqv (Var 9) (Eqv (Eqv F (Not (Var
1))) (Not (Var 5))))) (And (And (Eqv (Var 14) (Or (And (Var 13)
(Var 2)) (Or (And (Var 13) (Var 6)) (And (Var 2) (Var 6)))))
(Eqv (Var 10) (Eqv (Eqv (Var 13) (Not (Var 2))) (Not (Var 6)))))
(And (And (Eqv (Var 15) (Or (And (Var 14) (Var 3)) (Or (And (Var
14) (Var 7)) (And (Var 3) (Var 7))))) (Eqv (Var 11) (Eqv (Eqv
(Var 14) (Not (Var 3))) (Not (Var 7))))) (And (Eqv (Var 16) (Or
(And (Var 15) (Var 4)) (Or (And (Var 15) (Var 8)) (And (Var 4)
(Var 8))))) (Eqv (Var 12) (Eqv (Eqv (Var 15) (Not (Var 4))) (Not
(Var 8)))))))) (And (And (And (Eqv (Var 17) (Or (And (Not F)
(And (Var 1) (Var 5))) (And F (Or (Var 1) (Var 5))))) (Eqv (Var
9) (Or (And F (And (Var 1) (Var 5))) (Or (And F (And (Not (Var
1)) (Not (Var 5)))) (Or (And (Not F) (And (Var 1) (Not (Var
5)))) (And (Not F) (And (Not (Var 1)) (Var 5)))))))) (And (And
(Eqv (Var 18) (Or (And (Not (Var 17)) (And (Var 2) (Var 6)))
(And (Var 17) (Or (Var 2) (Var 6))))) (Eqv (Var 10) (Or (And
(Var 17) (And (Var 2) (Var 6))) (Or (And (Var 17) (And (Not (Var
2)) (Not (Var 6)))) (Or (And (Not (Var 17)) (And (Var 2) (Not
(Var 6)))) (And (Not (Var 17)) (And (Not (Var 2)) (Var 6))))))))
(And (And (Eqv (Var 19) (Or (And (Not (Var 18)) (And (Var 3)
(Var 7))) (And (Var 18) (Or (Var 3) (Var 7))))) (Eqv (Var 11)
(Or (And (Var 18) (And (Var 3) (Var 7))) (Or (And (Var 18) (And
(Not (Var 3)) (Not (Var 7)))) (Or (And (Not (Var 18)) (And (Var
3) (Not (Var 7)))) (And (Not (Var 18)) (And (Not (Var 3)) (Var
7)))))))) (And (Eqv (Var 20) (Or (And (Not (Var 19)) (And (Var
4) (Var 8))) (And (Var 19) (Or (Var 4) (Var 8))))) (Eqv (Var 12)
(Or (And (Var 19) (And (Var 4) (Var 8))) (Or (And (Var 19) (And
(Not (Var 4)) (Not (Var 8)))) (Or (And (Not (Var 19)) (And (Var
4) (Not (Var 8)))) (And (Not (Var 19)) (And (Not (Var 4)) (Var
8))))))))))) (Eqv (Var 16) (Var 20))))
tc 6 = (And (And (And (Eqv (Var 13) (Or (And F T) (Or (And F (Var 5))
(And T (Var 5))))) (Eqv (Var 9) (Eqv (Eqv F (Not T)) (Not (Var
5))))) (And (And (Eqv (Var 14) (Or (And (Var 13) F) (Or (And
(Var 13) (Var 6)) (And F (Var 6))))) (Eqv (Var 10) (Eqv (Eqv
(Var 13) (Not F)) (Not (Var 6))))) (And (And (Eqv (Var 15) (Or
(And (Var 14) F) (Or (And (Var 14) (Var 7)) (And F (Var 7)))))
(Eqv (Var 11) (Eqv (Eqv (Var 14) (Not F)) (Not (Var 7))))) (And
(Eqv (Var 16) (Or (And (Var 15) T) (Or (And (Var 15) (Var 8))
(And T (Var 8))))) (Eqv (Var 12) (Eqv (Eqv (Var 15) (Not T))
(Not (Var 8)))))))) (And (And (And (Eqv (Var 17) (Or (And (Not
F) (And T (Var 5))) (And F (Or T (Var 5))))) (Eqv (Var 9) (Or
(And F (And T (Var 5))) (Or (And F (And (Not T) (Not (Var 5))))
(Or (And (Not F) (And T (Not (Var 5)))) (And (Not F) (And (Not
T) (Var 5)))))))) (And (And (Eqv (Var 18) (Or (And (Not (Var
17)) (And F (Var 6))) (And (Var 17) (Or F (Var 6))))) (Eqv (Var
10) (Or (And (Var 17) (And F (Var 6))) (Or (And (Var 17) (And
(Not F) (Not (Var 6)))) (Or (And (Not (Var 17)) (And F (Not (Var
6)))) (And (Not (Var 17)) (And (Not F) (Var 6)))))))) (And (And
(Eqv (Var 19) (Or (And (Not (Var 18)) (And F (Var 7))) (And (Var
18) (Or F (Var 7))))) (Eqv (Var 11) (Or (And (Var 18) (And F
(Var 7))) (Or (And (Var 18) (And (Not F) (Not (Var 7)))) (Or
(And (Not (Var 18)) (And F (Not (Var 7)))) (And (Not (Var 18))
(And (Not F) (Var 7)))))))) (And (Eqv (Var 20) (Or (And (Not
(Var 19)) (And T (Var 8))) (And (Var 19) (Or T (Var 8))))) (Eqv
(Var 12) (Or (And (Var 19) (And T (Var 8))) (Or (And (Var 19)
(And (Not T) (Not (Var 8)))) (Or (And (Not (Var 19)) (And T (Not
(Var 8)))) (And (Not (Var 19)) (And (Not T) (Var 8)))))))))))
(Eqv (Var 16) (Var 20))))
tc 7 = Eqv (Not (Or (Var 1) (Or (Var 2) (Var 3))))
(And (Not (Var 1)) (And (Not (Var 2)) (Not (Var 3)) ))
tc 8 = (Eqv (Not (And (Var 1) (And (Var 2) (And (Var 3) (And (Var 4)
(And (Var 5) (And (Var 6) (And (Var 7) (And (Var 8) (And (Var 9)
(And (Var 10) (And (Var 11) (And (Var 12) (And (Var 13) (And
(Var 14) (And (Var 15) (Var 16))))))))))))))))) (Or (Not (Var
1)) (Or (Not (Var 2)) (Or (Not (Var 3)) (Or (Not (Var 4)) (Or
(Not (Var 5)) (Or (Not (Var 6)) (Or (Not (Var 7)) (Or (Not (Var
8)) (Or (Not (Var 9)) (Or (Not (Var 10)) (Or (Not (Var 11)) (Or
(Not (Var 12)) (Or (Not (Var 13)) (Or (Not (Var 14)) (Or (Not
(Var 15)) (Not (Var 16))))))))))))))))))
tc 9 = (Eqv (Not (Or (Var 1) (Or (Var 2) (Or (Var 3) (Or (Var 4) (Or
(Var 5) (Or (Var 6) (Or (Var 7) (Or (Var 8) (Or (Var 9) (Or (Var
10) (Or (Var 11) (Or (Var 12) (Or (Var 13) (Or (Var 14) (Or (Var
15) (Var 16))))))))))))))))) (And (Not (Var 1)) (And (Not (Var
2)) (And (Not (Var 3)) (And (Not (Var 4)) (And (Not (Var 5))
(And (Not (Var 6)) (And (Not (Var 7)) (And (Not (Var 8)) (And
(Not (Var 9)) (And (Not (Var 10)) (And (Not (Var 11)) (And (Not
(Var 12)) (And (Not (Var 13)) (And (Not (Var 14)) (And (Not (Var
15)) (Not (Var 16))))))))))))))))))
-- Test cases 10 to 21 were provided by Jonathan Pengelly
tc 10 = (And (Var 1) (Not (Var 1)))
tc 11 = (Or (And (Var 1) (Not (Var 2))) (And (Not (Var 1)) (Var 2)))
-- Modus Ponens test
tc 12 = (And (And (Var 1) (Imp (Var 1) (Var 2))) (Not (Var 2)))
-- Modus Tollens test
tc 13 = (And (And (Not (Var 2)) (Imp (Var 1) (Var 2))) (Var 1))
-- Double negation test
tc 14 = (Eqv (Var 1) (Not (Not (Var 1))))
-- Associativity
tc 15 = (Eqv (And (And (Var 1) (Var 2)) (Var 3))
(And (Var 1) (And (Var 2) (Var 3))))
-- De Morgan's rules
tc 16 = (Eqv (Not (Or (Var 1) (Var 2))) (And (Not (Var 1)) (Not (Var 2))))
-- Show that the following is not a tautology
tc 17 = (Imp (Imp (Var 1) (Var 3)) (Imp (Imp (Var 2) (Var 4))
(Imp (Or (Var 1) (Var 2)) (Var 3))))
-- Unsatisfiable set of clauses
tc 18 = (And (And (And (Or (Or (Var 1) (Var 2)) (Not (Var 3)))
(Or (Or (Var 1) (Var 2)) (Var 3))) (Or (Var 1) (Not (Var 2))))
(Not (Var 1)))
-- Tautology
tc 19 = (Imp (Var 1) (Imp (Var 2) (Var 1)))
tc 20 = T
tc 21 = F