Proper (empty) → 0.1.0.0

raw patch · 8 files changed

+385/−0 lines, 8 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, parsec

Files

LICENSE +30/−0
Proper.cabal +32/−0
Setup.hs +2/−0
src/Main.hs +23/−0
src/Proper/CNF.hs +52/−0
src/Proper/Clause.hs +31/−0
src/Proper/Sentence.hs +203/−0
test/Main.hs +12/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014, Dillon Huff++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS+OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.

+ Proper.cabal view

@@ -0,0 +1,32 @@+-- Initial Proper.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                Proper+version:             0.1.0.0+synopsis:	     An implementation of propositional logic in Haskell            +-- description:         +license:  		BSD3           +license-file:        LICENSE+-- author:              +-- maintainer:          +-- copyright:           +-- category:            +build-type:          Simple+cabal-version:       >=1.8++library+  hs-source-dirs:	src+  build-depends:	base==4.5.*, containers+  exposed-modules:	Proper.Sentence, Proper.CNF, Proper.Clause++executable Proper+  main-is:             Main.hs+  -- other-modules:       +  build-depends:       base ==4.5.*, containers, parsec+  hs-source-dirs:      src++executable Proper-tests+  main-is:             Main.hs+  -- other-modules:       +  build-depends:       base ==4.5.*, HUnit, containers, parsec+  hs-source-dirs:      test, src

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ src/Main.hs view

@@ -0,0 +1,23 @@+module Main(main) where++import System.Environment+import Proper.Lexer+import Proper.Parser+import Proper.Sentence+import System.IO+import Proper.Utils++main :: IO ()+main = do+  (fileName:rest) <- getArgs+  fHandle <- openFile fileName ReadMode+  thmString <- hGetContents fHandle+  let thm = processTheoremFile thmString+  case thm of+    Failed errMsg -> putStrLn errMsg+    Succeeded t -> do+      putStr $ show t+      putStrLn $ "\n\nis " ++ (show $ checkTheorem t)+  +processTheoremFile thmFileContents =+  (toTokens thmFileContents >>= parseTheoremToks)

+ src/Proper/CNF.hs view

@@ -0,0 +1,52 @@+module Proper.CNF(+  CNF, cnf, mergeCNFFormulas,+  naiveSAT)+       where++import Data.Map as M+import Data.Set as S+import Proper.Clause+import Proper.Utils++type CNF = Set Clause+  +cnf :: [Clause] -> CNF+cnf clauses = S.fromList clauses++mergeCNFFormulas :: [CNF] -> CNF+mergeCNFFormulas formulas = S.foldl S.union S.empty (S.fromList formulas)++literals :: CNF -> Set Atom+literals formula = S.foldl S.union S.empty (S.map (S.map literal) formula)++naiveSAT :: CNF -> Bool+naiveSAT formula = nSat simplifiedFormula allLits+  where+    simplifiedFormula = unitClauseSimplify formula+    allLits = literals simplifiedFormula+    +nSat :: CNF -> Set Atom -> Bool+nSat formula lits = case S.member S.empty formula of+  True -> False+  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)++unitClauseSimplify :: CNF -> CNF+unitClauseSimplify formula = S.foldl removeUnitClause formula unitClauses+  where+    unitClauses = S.filter (\s -> S.size s == 1) formula++removeUnitClause :: CNF -> Clause -> CNF+removeUnitClause formula c = remainingClauses+  where+    elemC = S.findMin c+    removeNegC = S.map (S.delete (negation elemC)) formula+    remainingClauses = S.filter (\s -> (not $ S.member elemC s)) removeNegC

+ src/Proper/Clause.hs view

@@ -0,0 +1,31 @@+module Proper.Clause(+  Atom, negation, lit, nLit, literal,+  Clause, clause, concatClause) where++import Data.Set as S++import Proper.Utils++data Atom =+  Lit Name |+  NLit Name+  deriving (Eq, Ord, Show)+  +negation :: Atom -> Atom+negation (Lit n) = NLit n+negation (NLit n) = Lit n++literal :: Atom -> Atom+literal (Lit n) = Lit n+literal (NLit n) = Lit n++lit name = Lit name+nLit name = NLit name++type Clause = Set Atom++concatClause :: Clause -> Clause -> Clause+concatClause c1 c2 = S.union c1 c2++clause :: [Atom] -> Clause+clause atoms = S.fromList atoms

+ src/Proper/Sentence.hs view

@@ -0,0 +1,203 @@+module Proper.Sentence(+  Sentence, checkTheorem,+  neg, con, dis, val, bic, imp,+  truthAssignment,+  evalSentence,+  isValidByTruthTable,+  toCNF, theorem) where++import Data.Map as M++import Proper.Clause+import Proper.CNF+import Proper.Utils++data Sentence =+  Val Name              |+  Neg Sentence          |+  Con Sentence Sentence |+  Dis Sentence Sentence |+  Bic Sentence Sentence |+  Imp Sentence Sentence+  deriving (Eq, Ord)++instance Show Sentence where+  show = showSent+  +showSent :: Sentence -> String+showSent (Val name) = 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++constants :: Sentence -> [Sentence]+constants (Val n) = [(Val n)]+constants (Neg s) = constants s+constants (Con s1 s2) = constants s1 ++ constants s2+constants (Dis s1 s2) = constants s1 ++ constants s2+constants (Bic s1 s2) = constants s1 ++ constants s2+constants (Imp s1 s2) = constants s1 ++ constants s2++type TruthAssignment = Map Sentence Bool++truthVal :: Sentence -> TruthAssignment -> 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 constNames constVals = M.fromList $ zip consts constVals+  where+    consts = Prelude.map val constNames++evalSentence :: TruthAssignment -> Sentence -> 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 = [TruthAssignment]++containsSentence :: Sentence -> TruthTable -> Bool+containsSentence s [] = False+containsSentence s tt = M.member s (head tt)++truthTable :: [Sentence] -> TruthTable+truthTable sents = Prelude.foldl addSentence [] sents++addSentence :: TruthTable -> Sentence -> TruthTable+addSentence tt s = if (containsSentence s tt)+  then tt+  else addNewSentence tt s++addNewSentence :: TruthTable -> Sentence -> TruthTable+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 :: Sentence -> TruthAssignment -> TruthAssignment+addCompoundSentence s ta = insert s sval ta+  where+    sval = evalSentence ta s++truthTableForSentence :: Sentence -> TruthTable+truthTableForSentence s = truthTable $ (constants s) ++ [s]+                          +isValidByTruthTable :: Sentence -> Bool+isValidByTruthTable s = and sTruthVals+  where+    sTruthTable = truthTableForSentence s+    sTruthVals = Prelude.map (truthVal s) sTruthTable+    +-- Format conversion functions+toCNF :: Sentence -> CNF+toCNF = cnf .+        cnfClauses .+        distributeDisjunction .+        pushNegation .+        removeImplication .+        removeBiconditional++cnfClauses :: Sentence -> [Clause]+cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2+cnfClauses s = [disjunctiveClause s]++disjunctiveClause :: Sentence -> Clause+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 (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 -> Sentence+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 -> Sentence+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 -> Sentence+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 = Thm [Sentence] Sentence+               deriving (Eq)+                        +instance Show Theorem where+  show = showThm+  +showThm :: Theorem -> 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 axioms hypothesis = Thm axioms hypothesis++checkTheorem :: Theorem -> Bool+checkTheorem (Thm axioms hypothesis) = not $ naiveSAT cnfFormNegThm+  where+    cnfAxioms = Prelude.map toCNF axioms+    cnfNotHypothesis = toCNF (neg hypothesis)+    cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)

+ test/Main.hs view

@@ -0,0 +1,12 @@+module Main(main) where++import Proper.CNFTests+import Proper.LexerTests+import Proper.ParserTests+import Proper.SentenceTests++main = do+  allSentenceTests+  allCNFTests+  allLexerTests+  allParserTests