Proper 0.1.0.0 → 0.2.0.0
raw patch · 4 files changed
+54/−54 lines, 4 files
Files
- Proper.cabal +3/−3
- src/Proper/CNF.hs +8/−8
- src/Proper/Clause.hs +8/−8
- src/Proper/Sentence.hs +35/−35
Proper.cabal view
@@ -2,13 +2,13 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: Proper-version: 0.1.0.0+version: 0.2.0.0 synopsis: An implementation of propositional logic in Haskell -- description: license: BSD3 license-file: LICENSE--- author: --- maintainer: +author: Dillon Huff +maintainer: Dillon Huff -- copyright: -- category: build-type: Simple
src/Proper/CNF.hs view
@@ -8,24 +8,24 @@ import Proper.Clause import Proper.Utils -type CNF = Set Clause+type CNF c = Set (Clause c) -cnf :: [Clause] -> CNF+cnf :: (Ord c) => [Clause c] -> CNF c cnf clauses = S.fromList clauses -mergeCNFFormulas :: [CNF] -> CNF+mergeCNFFormulas :: (Ord c) => [CNF c] -> CNF c mergeCNFFormulas formulas = S.foldl S.union S.empty (S.fromList formulas) -literals :: CNF -> Set Atom+literals :: (Ord c) => CNF c -> Set (Atom c) literals formula = S.foldl S.union S.empty (S.map (S.map literal) formula) -naiveSAT :: CNF -> Bool+naiveSAT :: (Ord c) => CNF c -> Bool naiveSAT formula = nSat simplifiedFormula allLits where simplifiedFormula = unitClauseSimplify formula allLits = literals simplifiedFormula -nSat :: CNF -> Set Atom -> Bool+nSat :: (Ord c) => CNF c -> Set (Atom c) -> Bool nSat formula lits = case S.member S.empty formula of True -> False False -> case S.size formula of@@ -39,12 +39,12 @@ nextFormula = unitClauseSimplify (S.insert unitClause formula) nextFormulaNeg = unitClauseSimplify (S.insert unitNegClause formula) -unitClauseSimplify :: CNF -> CNF+unitClauseSimplify :: (Ord c) => CNF c -> CNF c unitClauseSimplify formula = S.foldl removeUnitClause formula unitClauses where unitClauses = S.filter (\s -> S.size s == 1) formula -removeUnitClause :: CNF -> Clause -> CNF+removeUnitClause :: (Ord c) => CNF c -> Clause c -> CNF c removeUnitClause formula c = remainingClauses where elemC = S.findMin c
src/Proper/Clause.hs view
@@ -6,26 +6,26 @@ import Proper.Utils -data Atom =- Lit Name |- NLit Name+data Atom a =+ Lit a |+ NLit a deriving (Eq, Ord, Show) -negation :: Atom -> Atom+negation :: Atom a -> Atom a negation (Lit n) = NLit n negation (NLit n) = Lit n -literal :: Atom -> Atom+literal :: Atom a -> Atom a literal (Lit n) = Lit n literal (NLit n) = Lit n lit name = Lit name nLit name = NLit name -type Clause = Set Atom+type Clause c = Set (Atom c) -concatClause :: Clause -> Clause -> Clause+concatClause :: (Ord c) => Clause c -> Clause c -> Clause c concatClause c1 c2 = S.union c1 c2 -clause :: [Atom] -> Clause+clause :: (Ord a) => [Atom a] -> Clause a clause atoms = S.fromList atoms
src/Proper/Sentence.hs view
@@ -12,20 +12,20 @@ import Proper.CNF import Proper.Utils -data Sentence =- Val Name |- Neg Sentence |- Con Sentence Sentence |- Dis Sentence Sentence |- Bic Sentence Sentence |- Imp Sentence Sentence+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 Show Sentence where+instance Show s => Show (Sentence s) where show = showSent -showSent :: Sentence -> String-showSent (Val name) = name+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 ++ ")"@@ -39,7 +39,7 @@ imp s1 s2 = Imp s1 s2 val name = Val name -constants :: Sentence -> [Sentence]+constants :: Sentence s -> [Sentence s] constants (Val n) = [(Val n)] constants (Neg s) = constants s constants (Con s1 s2) = constants s1 ++ constants s2@@ -47,19 +47,19 @@ constants (Bic s1 s2) = constants s1 ++ constants s2 constants (Imp s1 s2) = constants s1 ++ constants s2 -type TruthAssignment = Map Sentence Bool+type TruthAssignment s = Map (Sentence s) Bool -truthVal :: Sentence -> TruthAssignment -> 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 :: [Name] -> [Bool] -> TruthAssignment+truthAssignment :: (Ord s) => [s] -> [Bool] -> TruthAssignment s truthAssignment constNames constVals = M.fromList $ zip consts constVals where consts = Prelude.map val constNames -evalSentence :: TruthAssignment -> Sentence -> Bool+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)@@ -73,21 +73,21 @@ s2Eval = evalSentence a s2 evalSentence a constant = truthVal constant a -type TruthTable = [TruthAssignment]+type TruthTable s = [TruthAssignment s] -containsSentence :: Sentence -> TruthTable -> Bool+containsSentence :: (Ord s) => Sentence s -> TruthTable s -> Bool containsSentence s [] = False containsSentence s tt = M.member s (head tt) -truthTable :: [Sentence] -> TruthTable+truthTable :: (Ord s, Show s) => [Sentence s] -> TruthTable s truthTable sents = Prelude.foldl addSentence [] sents -addSentence :: TruthTable -> Sentence -> TruthTable+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 :: TruthTable -> Sentence -> TruthTable+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@@ -95,22 +95,22 @@ ttTrue = Prelude.map (\ta -> M.insert c True ta) tt addNewSentence tt s = Prelude.map (addCompoundSentence s) tt -addCompoundSentence :: Sentence -> TruthAssignment -> TruthAssignment+addCompoundSentence ::(Ord s, Show s) => Sentence s -> TruthAssignment s -> TruthAssignment s addCompoundSentence s ta = insert s sval ta where sval = evalSentence ta s -truthTableForSentence :: Sentence -> TruthTable+truthTableForSentence :: (Ord s, Show s) => Sentence s -> TruthTable s truthTableForSentence s = truthTable $ (constants s) ++ [s] -isValidByTruthTable :: Sentence -> Bool+isValidByTruthTable :: (Ord s, Show s) => Sentence s -> Bool isValidByTruthTable s = and sTruthVals where sTruthTable = truthTableForSentence s sTruthVals = Prelude.map (truthVal s) sTruthTable -- Format conversion functions-toCNF :: Sentence -> CNF+toCNF :: (Ord s, Show s) => Sentence s -> CNF s toCNF = cnf . cnfClauses . distributeDisjunction .@@ -118,17 +118,17 @@ removeImplication . removeBiconditional -cnfClauses :: Sentence -> [Clause]+cnfClauses :: (Ord s, Show s) => Sentence s -> [Clause s] cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2 cnfClauses s = [disjunctiveClause s] -disjunctiveClause :: Sentence -> Clause+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 -> Sentence+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)@@ -138,7 +138,7 @@ q = removeImplication s2 removeImplication s = s -removeBiconditional :: Sentence -> Sentence+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)@@ -151,7 +151,7 @@ q = removeBiconditional s2 removeBiconditional (Val name) = (Val name) -pushNegation :: Sentence -> Sentence+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))@@ -159,7 +159,7 @@ pushNegation (Dis s1 s2) = Dis (pushNegation s1) (pushNegation s2) pushNegation s = s -distributeDisjunction :: Sentence -> Sentence+distributeDisjunction :: Sentence s -> Sentence s distributeDisjunction (Con p q) = Con (distributeDisjunction p) (distributeDisjunction q) distributeDisjunction (Dis p (Con q r)) = Con pdq pdr where@@ -180,22 +180,22 @@ distributeDisjunction s = s -- Theorem code-data Theorem = Thm [Sentence] Sentence+data Theorem s = Thm [Sentence s] (Sentence s) deriving (Eq) -instance Show Theorem where+instance Show s => Show (Theorem s) where show = showThm -showThm :: Theorem -> String+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] -> Sentence -> Theorem+theorem :: [Sentence s] -> Sentence s -> Theorem s theorem axioms hypothesis = Thm axioms hypothesis -checkTheorem :: Theorem -> Bool+checkTheorem :: (Ord s, Show s) => Theorem s -> Bool checkTheorem (Thm axioms hypothesis) = not $ naiveSAT cnfFormNegThm where cnfAxioms = Prelude.map toCNF axioms