Exercises Dynamic Epistemic Model Checking: Lecture 1

We assume that you have succeeded in installing the Haskell Platform from haskell.org/downloads.

The code that goes with the first lecture can be found in LFPMC.hs.

You should download this file, and also the file with the code of these exercises: Exercises1.hs. Use the definitions in your solutions to the exercises. For this you should insert your own Haskell definitions in your own copy of the file. Next load the file with the Haskell interpreter and check whether your definitions compile and work as expected.


> module Exercises1 where
> import LFPMC

Write implementations of

contradiction :: Form -> Bool
tautology :: Form -> Bool
-- logical entailment 
entails :: Form -> Form -> Bool
-- logical equivalence
equiv :: Form -> Form -> Bool

Next, check your definitions for correctness.


Here is a function for generating the list of all sublists of a given list:

> powlist :: Eq a => [a] -> [[a]]
> powlist [] = [[]]
> powlist (x:xs) = powlist xs ++ map (x:) (powlist xs)

Your task is to check whether this definition generates the expected number of sublists:


Let's consider an alternative way to define valuations. If the domain of propositions props is clear, valuations can be given as sublists of props.

Use this to define the list of all valuations for a given formula. You should use powlist from the previous exercise.

allVls :: Form -> [[Name]]

Give a function that takes a domain props of propositions and a sublist of that domain, and produces a valuation (an object of type Valuation).

The type of the conversion function is

names2valuation :: ([Name],[Name]) -> Valuation

Next, give a conversion function in the other direction.

valuation2names :: Valuation -> ([Name],[Name])

The first element of the output pair should give the domain, the second element the appropriate sublist.

How can you check that the two functions are inverses?


Use the valuations of type [Name] that you defined in a previous exercise to define an alternative evaluation function that evaluates with respect to a valuation of type . The type is:

evl :: [Name] -> Form -> Bool

Let's give an alternative definition of formulas that also has box and diamond formulas:

> data Frm = Prp Name
>          | Ng  Frm
>          | Cj [Frm]
>          | Dj [Frm]
>          | Imp Frm Frm 
>          | Eqv Frm Frm
>          | Box Frm
>          | Diam Frm
>          deriving Eq

Think of Box and Diam as S5 modalities.

These can be evaluated on non-empty lists of valuations.

Write a function

s5eval :: [[Name]] -> Frm -> Bool

that does this. Take the first element of the list of valuations as the current world.

Here are some examples: you should get


Finally, implement update with formulas that contain boxes and diamonds.

upd :: Frm -> [[Name]] -> [[Name]]
upds :: [Frm] -> [[Name]] -> [[Name]]

Give an example that makes clear that updates for the s5 language are no longer commutative.

Historical reference: this is the update system proposed by Frank Veltman in (Veltman 1996).


Veltman, F. 1996. “Defaults in Update Semantics.” Journal of Philosophical Logic, 221–61.