module Proper.Sentence(
Sentence, checkTheorem,
neg, con, dis, val, bic, imp,
truthAssignment,
evalSentence,
isValidByTruthTable,
toCNF, theorem,
bddCheckTaut) where
import Data.Foldable
import Data.Monoid
import Data.Map as M
import Proper.BDD
import Proper.Clause
import Proper.CNF
import Proper.Utils
data Sentence s =
Val s |
Neg (Sentence s) |
Con (Sentence s) (Sentence s) |
Dis (Sentence s) (Sentence s) |
Bic (Sentence s) (Sentence s) |
Imp (Sentence s) (Sentence s)
deriving (Eq, Ord)
instance Functor Sentence where
fmap f (Val v) = Val (f v)
fmap f (Neg s) = Neg (fmap f s)
fmap f (Con s1 s2) = Con (fmap f s1) (fmap f s2)
fmap f (Dis s1 s2) = Dis (fmap f s1) (fmap f s2)
fmap f (Bic s1 s2) = Bic (fmap f s1) (fmap f s2)
fmap f (Imp s1 s2) = Imp (fmap f s1) (fmap f s2)
instance Foldable Sentence where
foldMap f (Val v) = f v
foldMap f (Neg s) = foldMap f s
foldMap f (Con s1 s2) = mappend (foldMap f s1) (foldMap f s2)
foldMap f (Dis s1 s2) = mappend (foldMap f s1) (foldMap f s2)
foldMap f (Imp s1 s2) = mappend (foldMap f s1) (foldMap f s2)
foldMap f (Bic s1 s2) = mappend (foldMap f s1) (foldMap f s2)
instance Show s => Show (Sentence s) where
show = showSent
showSent :: (Show s) => (Sentence s) -> String
showSent (Val name) = show name
showSent (Neg s) = "~(" ++ show s ++ ")"
showSent (Con s1 s2) = "(" ++ show s1 ++ " & " ++ show s2 ++ ")"
showSent (Dis s1 s2) = "(" ++ show s1 ++ " | " ++ show s2 ++ ")"
showSent (Bic s1 s2) = "(" ++ show s1 ++ " <-> " ++ show s2 ++ ")"
showSent (Imp s1 s2) = "(" ++ show s1 ++ " -> " ++ show s2 ++ ")"
neg sent = Neg sent
con s1 s2 = Con s1 s2
dis s1 s2 = Dis s1 s2
bic s1 s2 = Bic s1 s2
imp s1 s2 = Imp s1 s2
val name = Val name
constantsF :: Sentence s -> [Sentence s]
constantsF s = foldMap (\n -> [Val n]) s
constants :: Sentence s -> [Sentence s]
constants s = foldMap (\n -> [Val n]) s
type TruthAssignment s = Map (Sentence s) Bool
truthVal :: (Ord s, Show s) => Sentence s -> TruthAssignment s -> Bool
truthVal s tt = case M.lookup s tt of
Just val -> val
Nothing -> error $ "Sentence not in truth table " ++ show s
truthAssignment :: (Ord s) => [s] -> [Bool] -> TruthAssignment s
truthAssignment constNames constVals = M.fromList $ zip consts constVals
where
consts = Prelude.map val constNames
evalSentence :: (Ord s, Show s) => TruthAssignment s -> Sentence s -> Bool
evalSentence a (Neg s) = not $ evalSentence a s
evalSentence a (Con s1 s2) = (evalSentence a s1) && (evalSentence a s2)
evalSentence a (Dis s1 s2) = (evalSentence a s1) || (evalSentence a s2)
evalSentence a (Imp s1 s2) = (not s1Eval) || s2Eval
where
s1Eval = evalSentence a s1
s2Eval = evalSentence a s2
evalSentence a (Bic s1 s2) = (s1Eval && s2Eval) || ((not s1Eval) && (not s2Eval))
where
s1Eval = evalSentence a s1
s2Eval = evalSentence a s2
evalSentence a constant = truthVal constant a
type TruthTable s = [TruthAssignment s]
containsSentence :: (Ord s) => Sentence s -> TruthTable s -> Bool
containsSentence s [] = False
containsSentence s tt = M.member s (head tt)
truthTable :: (Ord s, Show s) => [Sentence s] -> TruthTable s
truthTable sents = Prelude.foldl addSentence [] sents
addSentence :: (Ord s, Show s) => TruthTable s -> Sentence s -> TruthTable s
addSentence tt s = if (containsSentence s tt)
then tt
else addNewSentence tt s
addNewSentence :: (Ord s, Show s) => TruthTable s -> Sentence s -> TruthTable s
addNewSentence [] c@(Val n) = [truthAssignment [n] [True], truthAssignment [n] [False]]
addNewSentence tt c@(Val n) = ttFalse ++ ttTrue
where
ttFalse = Prelude.map (\ta -> M.insert c False ta) tt
ttTrue = Prelude.map (\ta -> M.insert c True ta) tt
addNewSentence tt s = Prelude.map (addCompoundSentence s) tt
addCompoundSentence ::(Ord s, Show s) => Sentence s -> TruthAssignment s -> TruthAssignment s
addCompoundSentence s ta = insert s sval ta
where
sval = evalSentence ta s
truthTableForSentence :: (Ord s, Show s) => Sentence s -> TruthTable s
truthTableForSentence s = truthTable $ (constants s) ++ [s]
isValidByTruthTable :: (Ord s, Show s) => Sentence s -> Bool
isValidByTruthTable s = Prelude.and sTruthVals
where
sTruthTable = truthTableForSentence s
sTruthVals = Prelude.map (truthVal s) sTruthTable
toCNF :: (Ord s, Show s) => Sentence s -> CNF s
toCNF = cnf .
cnfClauses .
distributeDisjunction .
pushNegation .
removeImplication .
removeBiconditional
cnfClauses :: (Ord s, Show s) => Sentence s -> [Clause s]
cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2
cnfClauses s = [disjunctiveClause s]
disjunctiveClause :: (Ord s, Show s) => Sentence s -> Clause s
disjunctiveClause (Dis s1 s2) = concatClause (disjunctiveClause s1) (disjunctiveClause s2)
disjunctiveClause (Val name) = clause [lit name]
disjunctiveClause (Neg (Val name)) = clause [nLit name]
disjunctiveClause s = error $ "Disjunctive clause contains " ++ show s
removeImplication :: Sentence s -> Sentence s
removeImplication (Neg s) = Neg $ removeImplication s
removeImplication (Con s1 s2) = Con (removeImplication s1) (removeImplication s2)
removeImplication (Dis s1 s2) = Dis (removeImplication s1) (removeImplication s2)
removeImplication (Imp s1 s2) = Dis (Neg p) q
where
p = removeImplication s1
q = removeImplication s2
removeImplication s = s
removeBiconditional :: Sentence s -> Sentence s
removeBiconditional (Neg s) = Neg $ removeBiconditional s
removeBiconditional (Con s1 s2) = Con (removeBiconditional s1) (removeBiconditional s2)
removeBiconditional (Dis s1 s2) = Dis (removeBiconditional s1) (removeBiconditional s2)
removeBiconditional (Imp s1 s2) = Imp (removeBiconditional s1) (removeBiconditional s2)
removeBiconditional (Bic s1 s2) = Con noBic1 noBic2
where
noBic1 = Imp p q
noBic2 = Imp q p
p = removeBiconditional s1
q = removeBiconditional s2
removeBiconditional (Val name) = (Val name)
pushNegation :: Sentence s -> Sentence s
pushNegation (Neg (Neg s)) = pushNegation s
pushNegation (Neg (Con s1 s2)) = Dis (pushNegation (Neg s1)) (pushNegation (Neg s2))
pushNegation (Neg (Dis s1 s2)) = Con (pushNegation (Neg s1)) (pushNegation (Neg s2))
pushNegation (Con s1 s2) = Con (pushNegation s1) (pushNegation s2)
pushNegation (Dis s1 s2) = Dis (pushNegation s1) (pushNegation s2)
pushNegation s = s
distributeDisjunction :: Sentence s -> Sentence s
distributeDisjunction (Con p q) = Con (distributeDisjunction p) (distributeDisjunction q)
distributeDisjunction (Dis p (Con q r)) = Con pdq pdr
where
pdq = distributeDisjunction $ Dis p q
pdr = distributeDisjunction $ Dis p r
distributeDisjunction (Dis (Con p q) r) = Con pdr qdr
where
pdr = distributeDisjunction $ Dis p r
qdr = distributeDisjunction $ Dis q r
distributeDisjunction (Dis p q) = case pd of
(Con r s) -> distributeDisjunction (Dis pd qd)
other -> case qd of
(Con r s) -> distributeDisjunction (Dis pd qd)
other -> Dis pd qd
where
pd = distributeDisjunction p
qd = distributeDisjunction q
distributeDisjunction s = s
data Theorem s = Thm [Sentence s] (Sentence s)
deriving (Eq)
instance Show s => Show (Theorem s) where
show = showThm
showThm :: (Show s) => Theorem s -> String
showThm (Thm axioms hyp) = "THEOREM\n" ++ axiomStr ++ "\n|=\n\n" ++ hypString
where
axiomStr = Prelude.concat $ Prelude.map (\a -> (show a) ++ "\n") axioms
hypString = show hyp
theorem :: [Sentence s] -> Sentence s -> Theorem s
theorem axioms hypothesis = Thm axioms hypothesis
checkTheorem :: (Ord s, Show s) => Theorem s -> Bool
checkTheorem (Thm axioms hypothesis) = not $ naiveSAT cnfFormNegThm
where
cnfAxioms = Prelude.map toCNF axioms
cnfNotHypothesis = toCNF (neg hypothesis)
cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)
bddCheckTaut :: (Ord s) => Sentence s -> Bool
bddCheckTaut sent = isTaut (toBDD sent)
toBDD :: (Ord s) => Sentence s -> BDD s
toBDD (Val n) = singletonBDD n
toBDD (Neg sent) = negBDD (toBDD sent)
toBDD (Dis f1 f2) = disBDD (toBDD f1) (toBDD f2)
toBDD (Con f1 f2) = conBDD (toBDD f1) (toBDD f2)
toBDD (Imp f1 f2) = impBDD (toBDD f1) (toBDD f2)
toBDD (Bic f1 f2) = bicBDD (toBDD f1) (toBDD f2)