Using resolution for testing modal satisfiability and building models
From MaRDI portal
Publication:1610669
DOI10.1023/A:1015067300005zbMath1005.03010MaRDI QIDQ1610669
Ullrich Hustadt, Renate A. Schmidt
Publication date: 20 August 2002
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)
Related Items
Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, Modal logics for reasoning about infinite unions and intersections of binary relations, Extracting models from clause sets saturated under semantic refinements of the resolution rule., Resolution with order and selection for hybrid logics, Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), First-Order Resolution Methods for Modal Logics, A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, Blocking and other enhancements for bottom-up model generation methods, A Tableau Calculus for Minimal Modal Model Generation
Uses Software
