Normal form for S5 models with one agent

S5 models, and modal logics in general, are an expansion on propositional logic, including several new operators, axioms and rules. I will not go into S5 models much since prior knowledge is assumed [Study guide part 1, http://www.ai.rug.nl/~rineke/unit1.ps]
The operators added to propositinal logic to form S5 logic can be seen in table 4.

table 4.

name	symbol	use
Known	K	$K p$
Maybe	M	$M q$

The normal form for S5$_{(1)}$ has the form of

$$\psi = \delta_1 \vee \delta_2 \vee .. \vee \delta_n$$

where

$$\delta = \alpha \wedge K\beta_1 \wedge K\beta_2 \wedge .. \we... ..._n \wedge M\gamma_1 \wedge M\gamma_2 \wedge .. \wedge M\gamma_m$$

and $\alpha$, $\beta_i$ and $\gamma_j$ are propositional formulas (in normal form)
Once again we will need rules to rewrite a given formula to normal form. As in propositional logic a distinction can be made between normalizing and simplifying the formula. To normalize only three basic equivalances are necessary in conjunction with the rules from propositoinal logic (table 5), but several derivated rules are helpfull (table 6).

table 5.

equivalence
$M\beta$	$\equiv$	$\neg K(\neg\beta)$
$K(\pi \vee (\lambda \wedge K\beta))$	$\equiv$	$(K(\pi \vee \lambda) \wedge K\beta) \vee ( K\pi \wedge \neg K\beta)$
$K(\pi \vee (\lambda \wedge M\beta))$	$\equiv$	$(K(\pi \vee \lambda) \wedge M\beta) \vee ( K\pi \wedge \neg M\beta)$

table 6.

nr	rule			case
1	$\neg K\beta$	$\equiv$	$M(\neg\beta)$
2	$\neg M\beta$	$\equiv$	$K(\neg\beta)$
3	$K(\pi \vee (\lambda \wedge K\beta))$	$\equiv$	$(K(\pi \vee \lambda) \wedge K\beta) \vee ( K\pi \wedge \neg K\beta)$
4	$K(\pi \vee (\lambda \wedge M\beta))$	$\equiv$	$(K(\pi \vee \lambda) \wedge M\beta) \vee ( K\pi \wedge \neg M\beta)$
5	$K(\lambda \wedge K\beta)$	$\equiv$	$K\lambda \wedge K\beta$	$\pi\Leftrightarrow\bot$
6	$K(\lambda \wedge M\beta)$	$\equiv$	$K\lambda \wedge M\beta$	$\pi\Leftrightarrow\bot$
7	$K(\pi \vee K\beta)$	$\equiv$	$K\beta \vee K\pi$	$\lambda\Leftrightarrow\top$
8	$K(\pi \vee M\beta)$	$\equiv$	$M\beta \vee K\pi$	$\lambda\Leftrightarrow\top$
9	$KK\beta$	$\equiv$	$K\beta$	$\pi\Leftrightarrow\bot$ and $\lambda\Leftrightarrow\top$
10	$KM\beta$	$\equiv$	$M\beta$	$\pi\Leftrightarrow\bot$ and $\lambda\Leftrightarrow\top$
11	$M((\pi \wedge \lambda) \vee (\pi \wedge M\beta))$	$\equiv$	$\neg((K(\neg\pi \vee \neg\lambda) \wedge \neg M\beta) \vee ( K\neg\pi \wedge M\beta))$
12	$M((\pi \wedge \lambda) \vee (\pi \wedge K\beta))$	$\equiv$	$\neg((K(\neg\pi \vee \neg\lambda) \wedge \neg K\beta) \vee ( K\neg\pi \wedge K\beta))$
13	$M(\lambda \vee M\beta)$	$\equiv$	$M\lambda \vee M\beta$	$\pi\Leftrightarrow\top$
14	$M(\lambda \vee K\beta)$	$\equiv$	$M\lambda \vee K\beta$	$\pi\Leftrightarrow\top$
15	$M(\pi \wedge M\beta)$	$\equiv$	$M\beta \wedge M\pi$	$\lambda\Leftrightarrow\bot$
16	$M(\pi \wedge K\beta)$	$\equiv$	$K\beta \wedge M\pi$	$\lambda\Leftrightarrow\bot$
17	$M(M\beta)$	$\equiv$	$M\beta$	$\pi\Leftrightarrow\top$ and $\lambda\Leftrightarrow\bot$
18	$M(K\beta)$	$\equiv$	$K\beta$	$\pi\Leftrightarrow\top$ and $\lambda\Leftrightarrow\bot$

Again frequent use of associative and commutative nature of 'and' and 'or' is needed unless the rules are generalized to incorporate them. Using the (generalized) rules from table 6 in conjunction with the rules from table 2 whenever applicable will normalize an s5$_{(1)}$ expression. Again simplification is advised to reduce the redundancy in the expression some helpfull rules are given in table 7.

table 7.

rule
$K(\top)$	$\equiv$	$\top$
$K(\bot)$	$\equiv$	$\bot$
$M(\top)$	$\equiv$	$\top$
$M(\bot)$	$\equiv$	$\bot$
$p \wedge Kp$	$\equiv$	$K p$
$Mp \wedge Kp$	$\equiv$	$K p$
$Mp \wedge p$	$\equiv$	$p$
$Kp \vee Mp$	$\equiv$	$Mp$
$p \vee Mp$	$\equiv$	$Mp$
$Kp \vee p$	$\equiv$	$p$
$K(\neg p) \wedge Mp$	$\equiv$	$\bot$
$K(\neg p) \wedge p$	$\equiv$	$\bot$
$M(\neg p) \wedge p$	$\equiv$	$\bot$
$K(\neg p) \vee Mp$	$\equiv$	$\top$
$K(\neg p) \vee p$	$\equiv$	$\top$
$M(\neg p) \vee p$	$\equiv$	$\top$

Most of these rules are pretty straightforward, and usage is on the same terms as before. But this is only a handfull, there are many more rules that can be derived from the axioms of S5 in varying complexity.