Portabilityportable
Stabilityprovisional
Safe HaskellNone

Dpfs.Simp

Description

Substitute all occurrencies of propositional variables to numbers. Transforms an propositional logic formula into an conjunctive normal form.

Synopsis

Documentation

cnf :: Int -> Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

cnf transformiert eine aussagenlogische Formel in eine Konjunktive Normalform

cnffast :: Int -> Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

cnffast transformiert eine aussagenlogische Formel in eine Konjunktive Normalform (lineare CNF)

pelimequiv :: Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

pelimequiv ersetzt Äquivalenzen innerhalb der Formel. (a = b) --> ((a => b) /\ (b => a))

pelimimpl :: Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

pelimimpl ersetzt Implikationen innerhalb der Formel. (a => b) --> (not a) // b

pelimnot :: Int -> Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

pelimnot ersetzt Vorkommen von (not Ptrue) bzw. (not Pfalse) zu Pfalse bzw. Ptrue

pelimTF :: Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

pelimTF löscht alle Vorkommen von Ptrue und Pfalse innerhalb der Formel.

pelimTFR :: Eq name => Pexpr name -> Pexpr name

deleteAll :: Eq a => a -> [a] -> [a]

pelimflat :: Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

pelimflat fasst verschachtelte Und- und Oder-Verknüpfungen zusammen.

porsublst :: Pexpr t -> [Pexpr t]

pandsublst :: Pexpr t -> [Pexpr t]

portop :: Pexpr t -> Bool

pandtop :: Pexpr t -> Bool

cnfRemoveTaut :: Pexpr (Int, [Int]) -> Pexpr (Int, [Int])

cnfRemoveTaut löscht Klauseln: -- indem Atome als Menge genau die festgelegte Menge besitzen, und -- indem ein Atom x mehrfach vorkommt und die Mengen dieser Atome disjunkt sind.

cnfRemoveTaut' :: (Eq a1, Eq a) => [Pexpr (a, [a1])] -> [Pexpr (a, [a1])]

cnfRemoveTaut'' :: (Eq a, Eq a1) => [Pexpr (a, [a1])] -> Bool

numPropSubs :: Int -> Pexpr String -> ([(String, Int)], Pexpr (Int, [Int]))

numPropSubs substituiert alle vorkommenden Variablen durch Int-Zahlen und zusätzlich wird der Typ PvarElem ersetzt durch Pvar. Das Ergebnis ist ein Tupel aus dem Variablen-Bindungen zu den substituierten Zahlen und der substituierte Liste selbst .

pVarNumber :: Int -> (Int, [(String, Int)]) -> Pexpr String -> ((Int, [(String, Int)]), Pexpr (Int, [Int]))

pVarNumber substituiert alle vorkommenden Variablen durch Int-Zahlen und ersetzt den Typ PvarElem durch Pvar (Num,Liste der Elemente).

pVarNumberList :: Int -> (Int, [(String, Int)]) -> ([Pexpr (Int, [Int])] -> Pexpr (Int, [Int])) -> [Pexpr String] -> ((Int, [(String, Int)]), Pexpr (Int, [Int]))

pSelemsToList :: Pexpr String -> [Int]

pSelemsToList' :: [Pexpr String] -> [Int]

showVar :: Pexpr t -> t