Theory matrices (for modal logics) using alphabetical monotonicity (Q687154)

The aim of the research reported here is to show a possible way in which the trends toward incorporating information about a certain theory into general purpose reasoning and, respectively, using an accessibility theory explicitely to enable theorem proving in modal logics, could be unified by a matrix characterization of validity. The method proposed by the author extends some techniques already known and is essentially based on tableau systems introduced by Smullyan in 1968. The structure of the paper can be described as follows: Some necessary preliminary basic concepts and results are presented in the first sections. In the third section of the paper, by removing some redundancies in the described system, a series of simplifications are demonstrated. Next, it is argued that if alphabetical monotonicity holds, the theory could be considered globally rather than locally. The derivation of a matrix characterization of validity is obtained in the fifth section. A series of comments concerning the extent to which the proposed technique is suited for automated reasoning in modal logics, and also some concluding remarks are given in the final part of the paper.