module Exercises2 where
import DEMO
import Data.List

{-

Construct an epistemic model with two agents $a$, $b$ and two propositions
$P 0$ and $Q 0$, with four worlds $0, 1, 2, 3$, and with the property
that $a$ knows about $P 0$ but not about $Q 0$, and $b$ knows about
$Q 0$ but not about $P 0$.

The declaration should be:

< example3 :: EpistM Int

-}

{-

What happens if you do an update of `example3` with a public
announcement of $p \lor q$? First think about what the correct answer
should be, next implement the update and check the result.

-}

{-

What happens if you do an update of `example3` with a public
announcement of $K_a p$ (where $p$ stands for the basic proposition
$P 0$? First think about what the correct answer should be, next
implement the update and check the result.

-}

{-

Can you extend the Drinking Logicians example to a model
where there are four drinking logicians?

You will need a model with four logicians $a,b,c,d$. The model should
be of the following type:

initBar2 :: EpistM (Bool,Bool,Bool,Bool)

-}

{-

In a case with four drinking logicians you need four updates.
Implement the updates and check the updating result. 

-}

{-

Now that you have seen the Drinking Logicians, can you
implement your own version of Muddy Children. Assume three
children, with two of them muddy and one clean.

Your initial situation should be

initMuddy :: EpistM (Bool,Bool,Bool)

Assume that `(True,True,False)` is the actual world: the first
and the second child are muddy, but the third child is clean.
The challenge is to get the correct representation of the
accessibility relations for the three children $a,b,c$.

-}

{-

If you have succeeded in defining the initial model
for the muddy children, next define the formulas that
you need for updating, and implement the updates.

-}

{-

Epistemic models and epistemic weight models have different types.
Still, any epistemic model can be lifted to an epistemic weight
model simply by letting the weight table for all agents assign
weight $1$ to all worlds.

Implement a function

< em2wem :: EpistM a -> EpistWM a

that achieves this.

-}

{-

Epistemic formulas of type `Frm a` can be translated into
probability formulas of type `Form a` by translating knowledge
as subjective certainty.

Implement a function

< frm2form :: Frm a -> Form a

that achieves this.

Next, check for some example models that this
translation preserves and reflects truth, when
you use the function `em2wem` to relate
the truth definitions for the two languages. 

-}