Lehman College, CUNY Graduate Center
Justification logics are connected to modal logics via realization theorems. These have both constructive and non-constructive proofs. Here we do two things. First we provide a new path to constructive realization proofs, going through an intermediate quasi-realization stage. Quasi-realizers are easier to produce than realizers, though like them they are constructed from cut-free proofs. Quasi-realizers in turn constructively convert to realizers, and this conversion is independent of the justification logic in question. The construction depends only on the structure of the formula involved.
The second thing we do is provide a Prolog implementation of quasi-realization, and quasi-realization to realization conversion, for the logic LP. Many other justification logics can obviously be treated similarly.
Our quasi-realization algorithm, and its implementation, assumes the underlying modal proof system S4 is based on tableaus. Since these may not be familiar to everybody, we provide a sketch of how tableaus work. Then we present our algorithms, our implementation, and a discussion of implementation behavior and design decisions.
We believe our algorithms are simple and straightforward. The original realization algorithm, for instance, needed the entire cut-free proof as input. Our quasi-realization algorithm works one formal proof step at a time. There is, in the literature, another realization construction that works one step at a time, but it requires extensive use of substitution while our quasi-realization algorithm does not. The conversion algorithm is, as noted above, independent of particular justification logics and so only needs to be understood once. It is only here that substitution is needed.
Both the program to compute realizations, and a tech report discussing the algorithm, necessary background, and the implementation, are available on the speaker’s web page:
Melvin Fitting is Professor Emeritus at Lehman College and the Graduate Center of the City University of New York. He received the 2012 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his outstanding contributions to tableau-based theorem proving in classical and non-classical logics, as well as to many other areas of Automated Reasoning, Logic Programming, and Philosophical Logic.