Resolution-based methods for modal logics
DOI10.1093/JIGPAL/8.3.265zbMATH Open0947.03014OpenAlexW2146427628MaRDI QIDQ4487263FDOQ4487263
Hans de Nivelle, Renate A. Schmidt, Ullrich Hustadt
Publication date: 7 November 2000
Published in: Logic Journal of the IGPL (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/bfd93c6e5f2e51892715f54d87df751816e30ef5
Recommendations
- scientific article; zbMATH DE number 3932427
- Resolution calculi for modal logics
- scientific article
- scientific article; zbMATH DE number 4027426
- Resolution in modal, description and hybrid logic
- Resolution theorem proving in reified modal logics
- The recursive resolution method for modal logic
- Publication:4945231
- Resolution-based calculi for modal and temporal logics
- scientific article; zbMATH DE number 4025402
surveydescription logicmodel generationdecision procedurestableauxguarded fragmentinference methodsmulti-modal logicsresolution methodssolvable classesextended propositional modal logics
Modal logic (including the logic of norms) (03B45) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)
Cited In (40)
- Blocking and other enhancements for bottom-up model generation methods
- Proof Complexity of Non-classical Logics
- Title not available (Why is that?)
- Local reductions for the modal cube
- Rewriting Conjunctive Queries over Description Logic Knowledge Bases
- Clausal resolution in a logic of rational agency
- A new methodology for developing deduction methods
- Deciding expressive description logics in the framework of resolution
- Deciding regular grammar logics with converse through first-order logic
- Resolution principles in possibilistic logic
- Clausal resolution for normal modal logics
- Title not available (Why is that?)
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- A tableau calculus for minimal modal model generation
- Using tableau to decide description logics with full role negation and identity
- First-Order Resolution Methods for Modal Logics
- Title not available (Why is that?)
- Model-Baded Abduction via Dual Resolution
- Simulation and Synthesis of Deduction Calculi
- Title not available (Why is that?)
- Hyperresolution for guarded formulae
- Resolution with order and selection for hybrid logics
- A description logic based situation calculus
- Using resolution for testing modal satisfiability and building models
- Title not available (Why is that?)
- Title not available (Why is that?)
- Modal Satisfiability via SMT Solving
- A Modal-Layered Resolution Calculus for K
- Constrained consequence
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Anti-prenexing and Prenexing for Modal Logics
- Title not available (Why is that?)
- Modal resolution in clausal form
- Using resolution for testing modal satisfiability and building models
- Title not available (Why is that?)
- Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving
- Modal Resolution
- Resolution calculi for non-normal modal logics
- Title not available (Why is that?)
- Title not available (Why is that?)
Uses Software
This page was built for publication: Resolution-based methods for modal logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4487263)
