Using resolution for testing modal satisfiability and building models
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].
- Using resolution for testing modal satisfiability and building models
- A proof procedure for hybrid logic with binders, transitivity and relation hierarchies
- scientific article; zbMATH DE number 5295699
- Fibred modal tableaux
- Resolution-based methods for modal logics
- scientific article; zbMATH DE number 1435945
- TABLEAUX: A general theorem prover for modal logics
- scientific article; zbMATH DE number 1215470
- Modal Satisfiability via SMT Solving
- Multimodal logic programming using equational and order-sorted logic
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- Blocking and other enhancements for bottom-up model generation methods
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- Resolution with order and selection for hybrid logics
- Using resolution for testing modal satisfiability and building models
- scientific article; zbMATH DE number 1696822 (Why is no real title available?)
- \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
- A tableau calculus for minimal modal model generation
- scientific article; zbMATH DE number 1215470 (Why is no real title available?)
- Using resolution for deciding solvable classes and building finite models
- Modal logics for reasoning about infinite unions and intersections of binary relations
- First-order resolution methods for modal logics
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Decidability Results for Saturation-Based Model Building
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
This page was built for publication: Using resolution for testing modal satisfiability and building models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1610669)
