diff --git a/logic.hs b/logic.hs new file mode 100644 index 0000000..07281e0 --- /dev/null +++ b/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)++""++(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 + + + diff --git a/makefile b/makefile new file mode 100644 index 0000000..985cb5b --- /dev/null +++ b/makefile @@ -0,0 +1,11 @@ + +COMP = ghc + +default: + $(COMP) test.hs logic.hs + +run: + ./test + + + diff --git a/test.hs b/test.hs new file mode 100644 index 0000000..9d786af --- /dev/null +++ b/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 + + +