Tableau to Quasi-Realization Algorithm
The construction in our algorithm involves a kind of backward induction. Suppose T is a closed annotated S4 block tableau. It is constructed using the tableau rules from Figures 5.13 and 5.15.
Eachbranchterminates with a closed block. To construct a quasi-realization tree counterpart
, we first say explicitly what the counterpart of a closed block is. And then, for each tableau rule application, if we know a counterpart for the conclusion (or conclusions when there is branching), we use this to compute the counterpart of the premise. Thus the construction of tableau
proceeds from root node downward to leaves, while the construction of a corresponding quasi-realization tree
proceeds from leaves upward to the root. A branch extension rule application extends only one branch—all others remain unchanged. Consequently the algorithm is stated in terms of branch extension rules applied to single branches. The rest of the quasi-realization tree being constructed does not change, so unaffected branches are not explicitly displayed.
In a few of the algorithm cases we need what can be called a trivial counterpart. This is for those cases where choices don't matter. For instance, if we have a modal tableau block that is closed because it contains T P and F P, the rest of the block doesn't matter, but any modal operators present still need to be turned into justification terms. To be definite, we take the trivial counter- 
7.9
More on the topic Tableau to Quasi-Realization Algorithm:
- Tableau to Quasi-Realization Algorithm Correctness
- Tableau to Quasi-Realization Algorithm
- Contents
- Classical Semantic Tableaus
- WhatWeDoHere