Alternative Translation Techniques for Propositional and First-Order Modal Logics

We describe and analyze techniques, other than the standard relational/functional methods, for translating validity problems of modal logics into first-order languages. For propositional modal logics we summarize the -as-Pow method, a complete and automatic translation into a weak set theory, and then describe an alternative method, which we call algebraic, that achieves the same full generality of -as-Pow but is simpler and computationally more attractive. We also discuss the relationships between the two methods, showing that -as-Pow generalizes to the first-order case. For first-order modal logics, we describe two extensions, of different degrees of generality, of -as-Pow to logics of rigid designators and constant domains.     

Single Step Tableaux for Modal Logics

Single Step Tableaux (SST) are the basis of a calculus for modal logics that combines different features of sequent and prefixed tableaux into a simple, modular, strongly analytic, and effective calculus for a wide range of modal logics.The paper presents a number of the computational results about SST (confluence, decidability, space complexity, modularity, etc.) and compares SST with other formalisms such as translation methods, modal resolution, and Gentzen-type tableaux. For instance, it discusses the feasibility and infeasibility of deriving decision procedures for SST and translation-based methods by replacing loop checking techniques with simpler termination checks.The complexity of searching for validity and logical consequence with SST and other methods is discussed. Minimal conditions on SST search strategies are proven to yield Pspace (and NPtime for S5 and KD45) decision procedures. The paper also presents the methodology underlying the construction of the correctness and completeness proofs.