Resolution in modal, description and hybrid logic (Q2772883)

A resolution-based proof procedure for modal, description and hybrid logic is provided. Modern modal theorem provers are generally based on tableau methods, and resolution is used for modal logic by translating modal languages to languages of first-order logic. In these cases, termination is ensured for the fragment of first-order logic corresponding to the modal language. NEWLINENEWLINENEWLINEResolution methods treating directly modal logic have been designed in the 80s and 90s. However, this task has encountered several difficulties. NEWLINENEWLINENEWLINEThe proposal of the authors in this paper is to treat directly with the language of modal logic but extended with mechanism of hybrid logic, as nominals and labelling. Nominals are used intuitively as names for possible worlds in a Kripkean semantics as Fitting style in his prefixed tableaux [\textit{M. Fitting}, Proof methods for modal and intuitionistic logics, Reidel, Dordrecht (1983; Zbl 0523.03013)]. Formulas in clauses can be seen as labelled formulas, and the set of clauses can be seen as a set of hybrid formulas. This use of hybrid machinery is at the metalogical level, but the authors use equally resolution for a basic hybrid language. On the other hand, the description logic \({\mathcal A}{\mathcal L},{\mathcal C}{\mathcal R}\) is viewed as a restricted hybrid logic.