c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder{-# OPTIONS -fglasgow-exts #-}

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maedermodule GMP.ModalKD where

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederimport GMP.GMPAS

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederimport GMP.ModalLogic

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederimport qualified Data.Set as Set

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maederdata KDrules = KDPR Int

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder | KDNR Int

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder deriving Show

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederdata Rchoice = P | N | O

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski deriving Eq

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance ModalLogic ModalKD KDrules where

af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski-- orderIns _ = True

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski contrClause n ma =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let p = Set.difference ma n

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in [Mimplies (Set.toList p) [aux]|aux <- Set.toList n]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ [Mimplies (Set.toList p) []]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski flagML _ = Sqr

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder parseIndex = return (ModalKD ())

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder matchR (Mimplies n p) =

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder case p of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder [] -> if (n == []) then [] else [KDNR (length n)]

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder _ -> [KDPR (length n)]

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder guessClause r =

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder case r of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski KDPR 0 -> [Pimplies [1] []]

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder KDPR n -> [Pimplies [n+1] [1..n]]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski KDNR n -> [Pimplies [] [1..n]]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-------------------------------------------------------------------------------

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-------------------------------------------------------------------------------

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski