Resolution in Modal Propositional Logic

摘要

In two papers from 1982, Louis Farinas del Cerro introduced an extension of theclassical resolution method to the propositional modal logics K,D,TS(4) and S(5). Subsequently further extensions to modal predicate logics have been published. The intuition behind the rules as defined by Farinas del Cerro has not become obvious to the present authors and also the rules seemed somewhat complicated. In the report the present authors define a system for resolution in modal propositional logics which is, at least to them, intuitively transparant. Soundness and completeness proofs for the systems K,D,TS(4) and S(5) are given in full detail.