TR-2007006: Realizing Substitution Instances of Modal Theorems
Melvin Fitting · CUNY Academic Works (City University of New York) · 2007
Suppose X is a theorem of S4, and a realization for X has been constructed.If X is a substitution instance of X, it is also a theorem of S4, and so is realizable, but the only available algorithm for producing a realization of X , so far, has been to apply a general realization algorithm to a cut-free proof of X .In effect we start over and the realization of X plays no role.It is the purpose of this report to present an algorithm for realizing substitution instances of a realizable formula that is, we believe, more efficient than a simple appeal to a general realization algorithm itself.