Proper 0.4.2.0 → 0.5.2.0
raw patch · 7 files changed
+302/−267 lines, 7 filesdep +sybdep ~base
Dependencies added: syb
Dependency ranges changed: base
Files
- Proper.cabal +5/−5
- src/Main.hs +1/−1
- src/Proper/CNF.hs +48/−23
- src/Proper/Clause.hs +11/−3
- src/Proper/Formula.hs +235/−0
- src/Proper/Sentence.hs +0/−233
- test/Main.hs +2/−2
Proper.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: Proper-version: 0.4.2.0+version: 0.5.2.0 synopsis: An implementation of propositional logic in Haskell description: Proper is both an executable theorem prover for Propositional logic and a library for incorporating propositional logic into other Haskell@@ -21,17 +21,17 @@ library hs-source-dirs: src- build-depends: base==4.5.*, containers- exposed-modules: Proper.Sentence, Proper.CNF, Proper.Clause, Proper.BDD+ build-depends: base < 6, containers, syb+ exposed-modules: Proper.Formula, Proper.CNF, Proper.Clause, Proper.BDD executable Proper main-is: Main.hs -- other-modules: - build-depends: base ==4.5.*, containers, parsec+ build-depends: base < 6, containers, parsec, syb hs-source-dirs: src executable Proper-tests main-is: Main.hs -- other-modules: - build-depends: base ==4.5.*, HUnit, containers, parsec+ build-depends: base < 6, HUnit, containers, parsec, syb hs-source-dirs: test, src
src/Main.hs view
@@ -3,7 +3,7 @@ import System.Environment import Proper.Lexer import Proper.Parser-import Proper.Sentence+import Proper.Formula import System.IO import Proper.Utils
src/Proper/CNF.hs view
@@ -1,13 +1,17 @@ module Proper.CNF(- CNF, cnf, mergeCNFFormulas,- naiveSAT)- where+ CNF, SatisfyingAssignment,+ cnf, mergeCNFFormulas,+ naiveSAT, naiveSATBool) where +import Control.Monad+import Data.Generics.Aliases+import Data.List as L import Data.Map as M import Data.Set as S import Proper.Clause import Proper.Utils +type SatisfyingAssignment l = Map l Bool type CNF c = Set (Clause c) cnf :: (Ord c) => [Clause c] -> CNF c@@ -16,34 +20,55 @@ mergeCNFFormulas :: (Ord c) => [CNF c] -> CNF c mergeCNFFormulas formulas = S.foldl S.union S.empty (S.fromList formulas) -literals :: (Ord c) => CNF c -> Set (Atom c)-literals formula = S.foldl S.union S.empty (S.map (S.map literal) formula)+literals :: (Ord c) => CNF c -> Set c+literals formula = S.map atom $ S.foldl S.union S.empty (S.map (S.map literal) formula) -naiveSAT :: (Ord c) => CNF c -> Bool-naiveSAT formula = nSat simplifiedFormula allLits+naiveSATBool :: (Ord c) => CNF c -> Bool+naiveSATBool formula = case naiveSAT formula of+ Just asg -> True+ Nothing -> False+ +-- A very naive implementation of DPLL+naiveSAT :: (Ord c) => CNF c -> Maybe (SatisfyingAssignment c)+naiveSAT formula = nSat formula allLits where- simplifiedFormula = unitClauseSimplify formula- allLits = literals simplifiedFormula+ allLits = literals formula -nSat :: (Ord c) => CNF c -> Set (Atom c) -> Bool+nSat :: (Ord c) => CNF c -> Set c -> Maybe (SatisfyingAssignment c) nSat formula lits = case S.member S.empty formula of- True -> False+ True -> Nothing False -> case S.size formula of- 0 -> True- _ -> (nSat nextFormula nextLits) || (nSat nextFormulaNeg nextLits)- where- nextLit = S.findMin lits- nextLits = S.delete nextLit lits- unitClause = clause [nextLit]- unitNegClause = clause [negation nextLit]- nextFormula = unitClauseSimplify (S.insert unitClause formula)- nextFormulaNeg = unitClauseSimplify (S.insert unitNegClause formula)+ 0 -> Just M.empty+ _ -> case S.size unitClauses of+ 0 -> pickLitAndSplit formula lits+ _ -> unitSimplify unitClause formula lits+ where+ unitClauses = S.filter (\c -> S.size c == 1) formula+ unitClause = S.findMin unitClauses -unitClauseSimplify :: (Ord c) => CNF c -> CNF c-unitClauseSimplify formula = S.foldl removeUnitClause formula unitClauses+pickLitAndSplit :: (Ord c) => CNF c -> Set c -> Maybe (SatisfyingAssignment c)+pickLitAndSplit formula lits = orElse trueAsg falseAsg where- unitClauses = S.filter (\s -> S.size s == 1) formula+ nextLit = S.findMin lits+ nextLits = S.delete nextLit lits+ trueRes = nSat (S.insert (clause [lit nextLit]) formula) nextLits+ falseRes = nSat (S.insert (clause [negation $ lit nextLit]) formula) nextLits+ trueAsg = liftM (M.insert nextLit True) trueRes+ falseAsg = liftM (M.insert nextLit False) falseRes +unitSimplify :: (Ord c) =>+ Clause c ->+ CNF c ->+ Set c ->+ Maybe (SatisfyingAssignment c)+unitSimplify unitClause formula lits = satResWithUnitAsg+ where+ simplifiedFormula = removeUnitClause formula unitClause+ litToSimplify = S.findMin unitClause+ tVal = assignTruthVal litToSimplify+ satRes = nSat simplifiedFormula lits+ satResWithUnitAsg = liftM (M.insert (atom litToSimplify) tVal) satRes+ removeUnitClause :: (Ord c) => CNF c -> Clause c -> CNF c removeUnitClause formula c = remainingClauses where
src/Proper/Clause.hs view
@@ -1,6 +1,7 @@ module Proper.Clause(- Atom, negation, lit, nLit, literal,- Clause, clause, concatClause) where+ Atom, atom, negation, lit, nLit, literal,+ Clause, clause, concatClause,+ assignTruthVal) where import Data.Set as S @@ -10,7 +11,11 @@ Lit a | NLit a deriving (Eq, Ord, Show)- ++assignTruthVal :: Atom l -> Bool+assignTruthVal (Lit _) = True+assignTruthVal (NLit _) = False+ negation :: Atom a -> Atom a negation (Lit n) = NLit n negation (NLit n) = Lit n@@ -18,6 +23,9 @@ literal :: Atom a -> Atom a literal (Lit n) = Lit n literal (NLit n) = Lit n++atom (Lit n) = n+atom (NLit n) = n lit name = Lit name nLit name = NLit name
+ src/Proper/Formula.hs view
@@ -0,0 +1,235 @@+module Proper.Formula(+ Formula, checkTheorem,+ neg, con, dis, val, bic, imp,+ truthAssignment,+ evalFormula,+ 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 Formula s =+ Val s |+ Neg (Formula s) |+ Con (Formula s) (Formula s) |+ Dis (Formula s) (Formula s) |+ Bic (Formula s) (Formula s) |+ Imp (Formula s) (Formula s)+ deriving (Eq, Ord)++instance Functor Formula 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 Formula 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 (Formula s) where+ show = showSent+ +showSent :: (Show s) => (Formula 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 :: Formula s -> [Formula s]+constantsF s = foldMap (\n -> [Val n]) s++constants :: Formula s -> [Formula s]+constants s = foldMap (\n -> [Val n]) s++type TruthAssignment s = Map (Formula s) Bool++truthVal :: (Ord s, Show s) => Formula s -> TruthAssignment s -> Bool+truthVal s tt = case M.lookup s tt of+ Just val -> val+ Nothing -> error $ "Formula 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++evalFormula :: (Ord s, Show s) => TruthAssignment s -> Formula s -> Bool+evalFormula a (Neg s) = not $ evalFormula a s+evalFormula a (Con s1 s2) = (evalFormula a s1) && (evalFormula a s2)+evalFormula a (Dis s1 s2) = (evalFormula a s1) || (evalFormula a s2)+evalFormula a (Imp s1 s2) = (not s1Eval) || s2Eval+ where+ s1Eval = evalFormula a s1+ s2Eval = evalFormula a s2+evalFormula a (Bic s1 s2) = (s1Eval && s2Eval) || ((not s1Eval) && (not s2Eval))+ where+ s1Eval = evalFormula a s1+ s2Eval = evalFormula a s2+evalFormula a constant = truthVal constant a+ +type TruthTable s = [TruthAssignment s]++containsFormula :: (Ord s) => Formula s -> TruthTable s -> Bool+containsFormula s [] = False+containsFormula s tt = M.member s (head tt)++truthTable :: (Ord s, Show s) => [Formula s] -> TruthTable s+truthTable sents = Prelude.foldl addFormula [] sents++addFormula :: (Ord s, Show s) => TruthTable s -> Formula s -> TruthTable s+addFormula tt s = if (containsFormula s tt)+ then tt+ else addNewFormula tt s++addNewFormula :: (Ord s, Show s) => TruthTable s -> Formula s -> TruthTable s+addNewFormula [] c@(Val n) = [truthAssignment [n] [True], truthAssignment [n] [False]]+addNewFormula 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+addNewFormula tt s = Prelude.map (addCompoundFormula s) tt++addCompoundFormula ::(Ord s, Show s) => Formula s -> TruthAssignment s -> TruthAssignment s+addCompoundFormula s ta = insert s sval ta+ where+ sval = evalFormula ta s++truthTableForFormula :: (Ord s, Show s) => Formula s -> TruthTable s+truthTableForFormula s = truthTable $ (constants s) ++ [s]+ +isValidByTruthTable :: (Ord s, Show s) => Formula s -> Bool+isValidByTruthTable s = Prelude.and sTruthVals+ where+ sTruthTable = truthTableForFormula s+ sTruthVals = Prelude.map (truthVal s) sTruthTable+ +-- Format conversion functions+toCNF :: (Ord s, Show s) => Formula s -> CNF s+toCNF = cnf .+ cnfClauses .+ distributeDisjunction .+ pushNegation .+ removeImplication .+ removeBiconditional++cnfClauses :: (Ord s, Show s) => Formula s -> [Clause s]+cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2+cnfClauses s = [disjunctiveClause s]++disjunctiveClause :: (Ord s, Show s) => Formula 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 :: Formula s -> Formula 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 :: Formula s -> Formula 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 :: Formula s -> Formula 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 :: Formula s -> Formula 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++-- Theorem code+data Theorem s = Thm [Formula s] (Formula 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 :: [Formula s] -> Formula s -> Theorem s+theorem axioms hypothesis = Thm axioms hypothesis++checkTheorem :: (Ord s, Show s) => Theorem s -> Bool+checkTheorem (Thm axioms hypothesis) = case naiveSAT cnfFormNegThm of+ Just asg -> False+ Nothing -> True+ where+ cnfAxioms = Prelude.map toCNF axioms+ cnfNotHypothesis = toCNF (neg hypothesis)+ cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)+ +-- BDD conversion code+ +bddCheckTaut :: (Ord s) => Formula s -> Bool+bddCheckTaut sent = isTaut (toBDD sent)++toBDD :: (Ord s) => Formula 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)
− src/Proper/Sentence.hs
@@ -1,233 +0,0 @@-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- --- Format conversion functions-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---- Theorem code-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)- --- BDD conversion code- -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)
test/Main.hs view
@@ -4,10 +4,10 @@ import Proper.CNFTests import Proper.LexerTests import Proper.ParserTests-import Proper.SentenceTests+import Proper.FormulaTests main = do- allSentenceTests+ allFormulaTests allCNFTests allLexerTests allParserTests