Resolution theorem proving in reified modal logics (Q1332644)

Non-classical logical systems are usually defined axiomatically. Set of axioms together with inference rules and rules of necessitation define a particular logic. An alternative approach is to define the semantics of the modal or temporal logic in first-order logic. This is known as the reified approach. In the reified approach to defining logical systems the semantics of the reified logics are defined by axioms in first-order logics. The present paper presents new empirical and theoretical work on theorem proving in reified logics. The rewriting methods and world-path methods used are not new but have been used in a novel application. The advantage of the approach is that the reified logics are represented in a logical system whose semantics and proof methods are well understood. First-order logic provides a sound framework for proving theorems of a reified logic. One consequence of adopting the reified approach is that if we wish to automate proofs for modal systems, then any of the standard theorem- proving methods for first-order logic can be used to implement a theorem prover for a reified modal logic.