Modal Theorem Proving: An Equational Viewpoint

摘要

This paper presents a method for automated deduction in first-order modal logic. The modal logic systems under consideration are arbitrary systems of type KD, KD4, KT, KT4, KT5 (though not all results hold for the latter), with the constant domain semantics, accepting flexible and rigid function and predicate symbols as well. The method works as follows. With any modal systemS, we associate an equational theoryE(S)in some classical first-order language with sorts (‘path logic’), and we define a translationTfrom modal to path logic, such that any formulaBis satisfiable with respect toSsemantics iffT(B)isE(S)-satisfiable. The question of modal theorem proving then amounts to theorem proving in some equational theories. In this paper we use Plotkin'sE-resolution, which provides‘free of charge’a framework immediately applicable to path logic. There is however one important problem left: some of the considered equational theories possess an associative operator, so that complete sets of unifiers (CSUs) may very well be infinite. The problem is overcome by observing that the formulae obtained by translation from modal logic belong to some fragment of path logic, characterized by the so-called‘unique prefix property’(UPP). Then a special Skolemization procedure preserving UPP is de-fined, and we give a unification algorithm for UPP terms, which computes