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

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancemodule ModalLogic where

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner

81ec673ac5ab1493568d9ef7798b752ab8ee0e61Felix Gabriel Manceimport GMPAS

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Text.ParserCombinators.Parsec

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Set as Set

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata PPflag = Sqr | Ang | None

5d801400993c9671010d244646936d8fd435638cChristian Maeder deriving Eq

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-------------------------------------------------------------------------------

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-- Modal Logic Class

aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mance-------------------------------------------------------------------------------

5d801400993c9671010d244646936d8fd435638cChristian Maederclass ModalLogic a b | a -> b, b -> a where

5d801400993c9671010d244646936d8fd435638cChristian Maeder-- orderIns :: (Formula a) -> Bool -- order insensitivity flag

5d801400993c9671010d244646936d8fd435638cChristian Maeder flagML :: (Formula a) -> PPflag -- primary modal operator flag

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance parseIndex :: Parser a -- index parser

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance matchR :: (RoClause a) -> [b] -- Rho matching

097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance guessClause :: b -> [Clause] -- clause guessing

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance{- default instance for the (negated) contracted clause choosing

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder - @ param n : the pseudovaluation

090c663fcc1593c66f39a0972326799a672760d5Christian Maeder - @ param ma : the modal atoms (excluding variables)

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu - @ return : the list of contracted clauses entailed by h -}

f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder contrClause :: (Ord a) =>

e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu Set.Set (Formula a) -> Set.Set (Formula a) -> [RoClause a]

e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu contrClause n ma =

feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Mance let p = Set.difference ma n

18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Mance pl = perm p

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance nl = perm n

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder in combineLit pl nl

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder-------------------------------------------------------------------------------

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance{- permute the elements of a set

863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance - @ param s : the set

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance - @ return : list of permuted items (stored as list) -}

f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maederperm :: (Ord t) => Set.Set t -> [[t]]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceperm s =

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance let perms l =

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder case l of

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance [] -> [[]]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance xs -> [x : ps | (x,ys) <- selections xs, ps <- perms ys]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance selections l =

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance case l of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [] -> []

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance x : xs -> (x,xs) : [(y,x:ys) | (y,ys) <- selections xs]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance in perms (Set.toList s)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance{- combine the positive and negative literals from the possible ones

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance - @ param l1 : list of modal atoms

0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mance - @ param l2 : list of modal atoms

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance - @ return : combined lists -}

852bd6145634dc2832b61c44678fe539bc1682d5Christian MaedercombineLit :: [[Formula a]] -> [[Formula a]] -> [RoClause a]

1a38107941725211e7c3f051f7a8f5e12199f03acmaedercombineLit l1 l2 =

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let assoc e l =

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance case l of

6033265e7b4ae660eff78e944213286863304903Mihai Codescu [] -> []

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance h:t -> Implies (e,h) : (assoc e t)

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance in case l1 of

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance [] -> []

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance x:xs -> (assoc x l2) ++ (combineLit xs l2)

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-------------------------------------------------------------------------------

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-------------------------------------------------------------------------------

68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder