An Illustrative Example

We give an example to illustrate how our algorithms work. We begin with an

Figure 7.2 S4 Annotated Block Tableau Proof

for the formula; it is a good exercise to construct a different one and extract a quasi-realization from it.

The block tableau shown in Figure 7.2 is converted to a quasi-realization tree using Algorithm 7.21, with the result shown in Figure 7.3. The work proceeds from bottom up.

Figure 7.3 Quasi-Realization Tree

In Figure 7.2,9 is an atomically closed block. The Atomic Cases of the algo-

7.11