# Finding Cheryl’s Birthday with DEMO

Following up on the Dynamic Epistemic Logic treatment of Cheryl’s Birthday Puzzle, Malvin Gattinger (ILLC Amsterdam) has formalized the problem in DEMO_S5, a Dynamic Epistemic Logic model checker written in Haskell by Jan van Eijck (CWI Amsterdam and ILLC). The original DEMO system was described in:

Jan van Eijck: “DEMO—a demo of epistemic modelling” In: Johan van Benthem, Dov Gabbay, and Benedikt Löwe, eds., Interactive Logic. Selected Papers from the 7th Augustus de Morgan Workshop, London. Vol. 1. Amsterdam University Press, 2007.

Go to Malvin’s page to download the source and documentation. Malvin’s original post follows, used under a Creative Commons Attribution 3.0 Unported license.

This report shows how to solve the famous riddle from Singapore (see NYTimes or SASMO on facebook) with dynamic epistemic logic and model checking in Haskell.

You can read it below or download the PDF or download the source files.

We use DEMO_S5 and a modified version of KRIPKEVIS.

```module CHERYL where
import Data.List
import Data.Function
import DEMO_S5
import KRIPKEVIS```

We first define the set of all possibilities:

```allpos :: [(Int, String)]
allpos = [ (15,"May"), (16,"May"), (19,"May"), (17,"June"), (18,"June"),
(14,"July"), (16,"July"), (14,"August"), (15,"August"), (17,"August") ]```

This forms the set of worlds in our initial model. Moreover, also the set of actual worlds is the full set, hence `allpos` occurs twice in the definition below. The two elements of `rels` define the epistemic relations of Albert and Bernard. Instead of listing explicitly which possibilities they can distinguish we use haskell functions to say that they confuse the same day and the same month, respectively.

```initCheryl :: EpistM (Int,String)
initCheryl = Mo allpos [a,b] [] rels allpos where
rels = [ ( a, groupBy ((==) `on` snd) allpos ), ( b, groupBy ((==) `on` fst) (sortBy (compare `on` fst) allpos) ) ]```

This is the initial model with all possibilities:

The formula saying that i knows Cheryl’s birthday is defined as the disjunction over all statements of the form “Agent i knows that the birthday is s”:

```knWhich :: Agent -> Form (Int, [Char])
knWhich i = Disj [ Kn i (Info s) | s <- allpos ]```

Now we update the model three times, using the function `upd_pa` for public announcements.

First with Albert: I don’t know when Cheryl’s birthday is and I know that Bernard does not know.

`model2 = upd_pa initCheryl (Conj [Ng \$ knWhich a, Kn a \$ Ng (knWhich b)])`

The second announcement by Bernard: “Now I know when Cheryl’s birthday is.”

`model3 = upd_pa model2 (knWhich b)`

Finally, Albert says: “Now I also know when Cheryl’s birthday is.”

`model4 = upd_pa model3 (knWhich a)`

Lastly, this helper function uses `texModel` from our modified `KRIPKEVIS` module to generate the drawings:

```myTexModel :: EpistM (Int,String) -> String -> IO String
myTexModel (Mo states _ _ rels pointed) fn =
texModel showState showAg showVal "" (VisModel states rels [(s,0)|s<-states] pointed) fn
where
showState (n,string) = (show n) ++ string
showVal _ = ""
showAg i = if i==a then "Albert" else "Bernard"```