GenericSequent.hs revision f00edd94c598adc73dc4f6005d79d2295e463da5
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{-# OPTIONS -fglasgow-exts #-}
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule GenericSequent where
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian Maederimport ModalLogic
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CombLogic
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder--import Data.Map as Map
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Generate all possible clauses out of a list of atoms
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiallClauses :: [a] -> [Clause a]
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiallClauses x = case x of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder h:t -> let addPositive c (Implies n p) = Implies n (c:p)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder addNegative c (Implies n p) = Implies (c:n) p
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in List.map (addPositive h) (allClauses t) ++
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder List.map (addNegative h) (allClauses t)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> [Implies [] []]
85ebda7270c6883b503d3bde4757033c09c25644Christian Maeder-- | Extract the modal atoms from a formula
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedergetMA :: Eq a => Boole a -> [Boole a]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedergetMA x = case x of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder And phi psi -> (getMA phi) `List.union` (getMA psi)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder Not phi -> getMA phi
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz At phi -> [At phi]
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | Substitution of modal atoms within a "Boole" expression
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedersubst :: Eq a => Boole a -> Clause (Boole a) -> Boole a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedersubst x s@(Implies neg pos) =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder And phi psi -> And (subst phi s) (subst psi s)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder Not phi -> Not (subst phi s)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder _ -> if (elem x neg) then F
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder else if (elem x pos) then T
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- | Evaluation of an instantiated "Boole" expression
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedereval :: Boole a -> Bool
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maedereval x = case x of
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder And phi psi -> (eval phi) && (eval psi)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Not phi -> not (eval phi)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- | DNF: disjunctive normal form of a Boole expression
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskidnf :: (Eq a) => Boole a -> [Clause (Boole a)]
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskidnf phi = List.filter (\x -> eval (subst phi x)) (allClauses (getMA phi))
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- | CNF: conjunctive normal form of a Boole expression
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskicnf :: (Eq a) => Boole a -> [Clause (Boole a)]
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskicnf phi = List.map (\(Implies x y) -> Implies y x) (dnf (Not phi))
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- | Generic Provability Function
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiprovable :: (Eq a, Form a b c) => Boole a -> Bool
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederprovable _ = True
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederprovable phi =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder let unwrap (Subst x) = Map.elems x
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in all (\c -> any (all provable) (List.map unwrap.snd (match c))) (cnf phi)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | Generic Satisfiability Function
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedersat :: (Eq a, Form a b c) => Boole a -> Bool
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedersat phi = not $ provable $ neg phi
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Function for "normalizing" negation
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederneg :: Eq a => Boole a -> Boole a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederneg phi = case phi of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Not psi -> psi