Arbitrary announcement in belief revision

We provide a pedagogical demonstration for belief revision. The following picture depicts the possible worlds for agent 1 and 2. You can make private announcements to agent 1 or agent 2 and public announcements. You can also ask for existence of a public announcement so agent 1 and agent 2 believe some properties.


Agent 1	Agent 2

Specified announcement

Arbitrary announcement

We want:

that agent 1 believes
that agent 2 believes

There is no such public announcement

Help on the syntax for formulas

Propositions are rainBow, Cloud, Rain and Sun. Letters b, c, r, s are abbreviations for respectively rainBow, Cloud, Rain and Sun.
((b or c) and (r or s)) is a well-formed formula. Formulas are fully parenthesized.
(s <-> (r or b)) is a well-formed formula.
(s -> (not r)) is a well-formed formula.