Using resolution for testing modal satisfiability and building models (Q1610669)

A translation-based decision procedure for a multimodal logic is presented. Specifically, the paper deals with the logic \(K_{(m)}(\cap,\cup,\smile)\), which can be seen as an extension of the basic tense logic \(K_t\) with intersection and union of relations (also converse relations are allowed, but not complementation of relations). The syntax and semantics of this logic is defined, and extensions with first-order frame properties or axiom schemas are presented. The resolution framework adopted by the authors is that of \textit{L. Bachmair} and \textit{H. Ganzinger} [``Resolution theorem proving'', in: A. Robinson et al. (eds.), Handbook of automated reasoning, Amsterdam: North Holland/Elsevier, 19-99 (2001; Zbl 0993.03008)]. The application of resolution is done via a structure-preserving transformation into clause form, in order to keep a link between the structure of modal formulae and their translated clause form. The procedure is based on a selection refinement of resolution, adopting a different approach to ordered refinements. It is interesting to stress that the method also finds models for satisfiable input formulae. It is shown that the proposed selection-based decision procedure can polynomially simulate a tableaux calculus in the spirit of \textit{F. Massacci} [``Simplification: A general constraint propagation technique for propositional and modal tableaux'', Lect. Notes Comput. Sci. 1397, 217-231 (1998; Zbl 0903.03012)]. The last section of the paper describes a first implementation of the selection-based resolution calculus and some experiments and comparative results. The implementation is performed as an extension of the theorem prover SPASS [see \textit{C. Weidenbach} et al., ``SPASS v0.77'', in: The CADE-14 ATP system competion, J. Autom. Reasoning 21, No. 1, 99-134 (1998; Zbl 0916.68141), p. 113].