159 lines
4.6 KiB
Haskell
159 lines
4.6 KiB
Haskell
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
|
|
|
|
|
|
|