Using resolution for testing modal satisfiability and building models
From MaRDI portal
Recommendations
- 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
Cited in
(17)- 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)
