1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# OPTIONS -fglasgow-exts #-}

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maedermodule GMP.ModalLogic where

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariimport GMP.GMPAS

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariimport Text.ParserCombinators.Parsec

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport qualified Data.Set as Set

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederdata PPflag = Sqr | Ang | None

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder deriving Eq

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder-------------------------------------------------------------------------------

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder-- Modal Logic Class

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder-------------------------------------------------------------------------------

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegariclass ModalLogic a b | a -> b, b -> a where

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder-- orderIns :: Set.Set (Formula a) -> Bool -- order insensitivity flag

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari flagML :: (Formula a) -> PPflag -- primary modal operator flag

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari parseIndex :: Parser a -- index parser

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder matchR :: (ModClause a) -> [b] -- Rho matching

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder guessClause :: b -> [PropClause] -- clause guessing

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari{- default instance for the (negated) contracted clause choosing

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari - @ param n : the pseudovaluation

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder - @ param ma : the modal atoms (excluding variables)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari - @ return : the list of contracted clauses entailed by h -}

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari contrClause :: (Ord a)=>Set.Set(Formula a)->Set.Set(Formula a)->[ModClause a]

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari contrClause n ma =

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder let p = Set.difference ma n

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari pl = perm p

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari nl = perm n

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari in combineLit pl nl

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari-------------------------------------------------------------------------------

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari{- permute the elements of a set

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder - @ param s : the set

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder - @ return : list of permuted items (stored as list) -}

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariperm :: (Ord t) => Set.Set t -> [[t]]

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariperm s =

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari let perms l =

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder case l of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> [[]]

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari xs -> [x : ps | (x,ys) <- selections xs, ps <- perms ys]

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari selections l =

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari case l of

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari [] -> []

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder x : xs -> (x,xs) : [(y,x:ys) | (y,ys) <- selections xs]

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari in perms (Set.toList s)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari{- combine the positive and negative literals from the possible ones

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder - @ param l1 : list of modal atoms

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari - @ param l2 : list of modal atoms

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari - @ return : combined lists -}

acc049a844d19fb294ce7f68742390dee87447dcDaniel CalegaricombineLit :: [[Formula a]] -> [[Formula a]] -> [ModClause a]

acc049a844d19fb294ce7f68742390dee87447dcDaniel CalegaricombineLit l1 l2 = [Mimplies x y | x <- l1, y <- l2]

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari-------------------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-------------------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder