add files

logic.hs

@@ -0,0 +1,158 @@
+module Logic where
+import Data.List
+{-====================================================
+=================== Aussagenlogik ====================
+====================================================-}
+dict2func :: (Eq a) => [(a,b)] -> (a -> b)
+dict2func d = \x -> (head [b |(a,b)<-d, a==x ])
+
+type Binary = [Int]
+
+toBin :: Int -> Binary
+toBin 0 = [0]
+toBin 1 = [1]
+toBin n
+    | n `mod` 2 == 0 = toBin (n `div` 2) ++ [0]
+    | otherwise = toBin (n `div` 2) ++ [1]
+
+bloatBin :: Int -> Binary -> Binary
+bloatBin n x
+    | n==(length x) = x
+    | otherwise = [0| i<-[1..n-(length x)]] ++ x
+
+type Belegung = Char -> Bool
+data Formel = TAUTO
+            | ABSURD
+            | Atom Char 
+            | NOT Formel
+            | Formel `OR` Formel
+            | Formel `AND` Formel
+            | Formel `THEN` Formel
+            | Formel `EQUY` Formel
+            | Formel `XOR` Formel
+
+instance Show Formel where
+    show TAUTO = "T" 
+    show ABSURD = "_|_"
+    show (Atom a) = [a] 
+    show (NOT f) = "(-"++(show f)++")"
+    show (a `AND` b) = "("++(show a)++"^"++(show b)++")"
+    show (a `OR` b) = "("++(show a)++"v"++(show b)++")"
+    show (a `THEN` b) = "("++(show a)++"=>"++(show b)++")"
+    show (a `EQUY` b) = "("++(show a)++"<=>"++(show b)++")"
+    show (a `XOR` b) = "("++(show a)++"<x>"++(show b)++")"
+
+noArrows :: Formel -> Formel
+noArrows TAUTO = TAUTO
+noArrows ABSURD = ABSURD
+noArrows (Atom a) = Atom a
+noArrows (NOT a) = NOT $ noArrows a
+noArrows (a `AND` b) = (noArrows a) `AND` (noArrows b)
+noArrows (a `OR` b) = (noArrows a) `OR` (noArrows b)
+noArrows (a `THEN` b) = (NOT $ noArrows a) `OR` noArrows b
+noArrows (a `EQUY` b) = (noArrows $ a `THEN` b) `AND` (noArrows $ b `THEN` a)
+
+nnf :: Formel -> Formel
+nnf TAUTO = TAUTO
+nnf ABSURD = ABSURD
+nnf (Atom a) = Atom a             --literal pos
+nnf (NOT (Atom a)) = NOT (Atom a) --literal neg
+nnf (NOT TAUTO) = ABSURD
+nnf (NOT ABSURD) = TAUTO
+nnf (NOT (NOT f)) = nnf f --double neg
+nnf (a `AND` b) = (nnf a) `AND` (nnf b)
+nnf (a `OR` b) = (nnf a) `OR` (nnf b)
+nnf (NOT (a `OR` b)) = (nnf $ NOT a) `AND` (nnf $ NOT b) --deMorgan 1
+nnf (NOT (a `AND` b)) = (nnf $ NOT a) `OR` (nnf $ NOT b) --deMorgan 2
+nnf (a `THEN` b) = nnf $ noArrows $ a `THEN` b             --remove arrows
+nnf (a `EQUY` b) = nnf $ noArrows $ a `EQUY` b             --remove arrows
+nnf (NOT (a `THEN` b)) = nnf $ NOT $ noArrows $ a `THEN` b --remove arrows
+nnf (NOT (a `EQUY` b)) = nnf $ NOT $ noArrows $ a `EQUY` b --remove arrows
+
+evalform :: Formel -> Belegung -> Bool
+evalform TAUTO _ = True
+evalform ABSURD _ = False
+evalform (Atom a) f = f a
+evalform (NOT a) f = not (evalform a f)
+evalform (a `AND` b) f = (evalform a f) && (evalform b f)
+evalform (a `OR` b) f = (evalform a f) || (evalform b f)
+evalform (a `THEN` b) f = evalform (noArrows $ a `THEN` b) f
+evalform (a `EQUY` b) f = evalform (noArrows $ a `EQUY` b) f
+
+formLen :: Formel -> Int
+formLen ABSURD = 1
+formLen TAUTO = 1
+formLen (Atom c) = 1
+formLen (NOT a) = 1 + (formLen a)
+formLen (a `AND` b) = (formLen a) + 1 + (formLen b)
+formLen (a `OR` b) = (formLen a) + 1 + (formLen b)
+formLen (a `THEN` b) = formLen $ noArrows $ a `THEN` b
+formLen (a `EQUY` b) = formLen $ noArrows $ a `EQUY` b
+
+atoms :: Formel -> [Char]
+atoms ABSURD = []
+atoms TAUTO = []
+atoms (Atom c) = [c]
+atoms (NOT a) = atoms a
+atoms (a `AND` b) = (atoms a) `union` (atoms b)
+atoms (a `OR` b) = (atoms a) `union` (atoms b)
+atoms (a `THEN` b) = (atoms a) `union` (atoms b)
+atoms (a `EQUY` b) = (atoms a) `union` (atoms b)
+atoms (a `XOR` b) = (atoms a) `union` (atoms b)
+
+allAlpha :: Int -> [Binary]
+allAlpha n = let f = (bloatBin n).toBin in [ f x |x<-[0..(2^n)-1] ]
+
+numAtoms :: Formel -> Int
+numAtoms = length.atoms
+
+--------------------------------------------------------------
+
+{-
+instance Eq Formel where
+    TAUTO == TAUTO = True
+    ABSURD == ABSURD = True
+    (Atom a) == (Atom b) = a==b
+    (a `OR` b) == (b `OR` a) = True
+    (a `AND` b) == (b `AND` a) = True
+-}
+
+
+--todo
+str2form :: String -> Formel
+str2form s
+    | (head s)=='-' = NOT $ str2form $ tail s
+    | (head s) `elem` "ABCDEFGHIJKLMNOPQRSTUVWXYZ" = Atom $ head s
+    | otherwise = Atom 'A'
+
+
+
+{-
+
+A B C | AvB | BvC
+-------------------------
+0 0 0 |
+0 0 1 |
+
+-}
+
+truthTable :: Formel -> IO()
+truthTable f = do
+    let n = length $ atoms f
+    let r = 2^n
+    print $ "---"++(atoms f)++"---"
+    sequence_ [print x | x <-allAlpha n]
+    print "------"
+
+showInfo :: Formel -> IO()
+showInfo f = do
+    print $ "Formula:"++(show f)
+    print $ "NNF:    "++(show $ nnf f)
+    print $ "Length: "++(show $ formLen f)
+    print $ "Atoms:  "++(atoms f)
+    truthTable f
+
+--https://www.google.de/search?q=ukraine+nazis&tbm=isch&ei=Sb1wVdjyMMK8swHGxoPgDQ
+
+
+

makefile

@@ -0,0 +1,11 @@
+
+COMP = ghc
+
+default:
+	$(COMP) test.hs logic.hs
+
+run:
+	./test
+
+
+

test.hs

@@ -0,0 +1,15 @@
+import Logic
+
+main = do
+        --let alpha = dict2func [('A',True),('B',False),('C',True)]
+        let alpha = dict2func $ zip ['A','B','C'] [True,False,True]
+
+            a = Atom 'A'
+            b = Atom 'B'
+            c = Atom 'C'
+            --f = (NOT (NOT ((NOT a) `THEN` (b `EQUY`(NOT a)))))
+            f = NOT $ NOT $ NOT a `THEN` (b `EQUY` NOT a)
+        showInfo f
+
+
+