© 1992 by Oxford University Press
Original Articles |
Modal Theorem Proving: An Equational Viewpoint
*Sociét´e des avions M.Dassault 78 quai Marcel Dassault, 92210 Saint-Cloud, France.
Laboratoire d'Informatique, Université de Caen 14032 Caen Cedex, France
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 system S, we associate an equational theory E(S) in some classical first-order language with sorts (‘path logic’), and we define a translation T from modal to path logic, such that any formula B is satisfiable with respect to S semantics iff T(B) is E(S)-satisfiable. The question of modal theorem proving then amounts to theorem proving in some equational theories. In this paper we use Plotkin's E-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 finite CSUs.