Using resolution for testing modal satisfiability and building models

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)

zbMATH Keywords

modal logictableauxresolutionmodel generationautomated deductiondecision proceduremultimodal logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items (10)

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

• SPASS

This page was built for publication: Using resolution for testing modal satisfiability and building models