Matrix proof methods for modal logics

Abstract

We present matrix proof systems for both constant- and varying-domain versions of the first-order modal logics K, K4, D, D4, T, 84 and 86 based on modal versions of Herbrand's Theorem specifically formulated to support efficient automated proof search. The systems treat the mil modal language (no normal-forming) and admit straightforward structure sharing implementations. A key fsature of our approach is the use of a specialised unification algorithm to reflect the conditions on the accessibility relation for a given logic. The matrix system for one logic differs from the matrix eystem for another only in the nature of this unification algorithm. In addition, proof search may be interpreted as constructing generalised proof trees in an appropriate tableau- or sequent-based proof system. This facilitates the use of the matrix systems within interactive environments.