BDD-based decision procedures for the modal logic K ★

DOI10.3166/jancl.16.169-207zbMath1184.68466OpenAlexW2068815633MaRDI QIDQ3647260

Guoqiang Pan, Moshe Y. Vardi, Ulrike Sattler

Publication date: 30 November 2009

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3166/jancl.16.169-207

zbMATH Keywords

modal logicbinary decision diagram

Mathematics Subject Classification ID

Related Items (11)

Logic programming approach to automata-based decision procedures ⋮ One-Pass Tableaux for Computation Tree Logic ⋮ Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic ⋮ Efficiently Deciding μ-Calculus with Converse over Finite Trees ⋮ An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability ⋮ Fuzzy Description Logic Reasoning Using a Fixpoint Algorithm ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ : A Resolution-Based Prover for Multimodal K ⋮ Efficient local reductions to basic modal logic ⋮ Query Answering in Description Logics: The Knots Approach ⋮ Local is best: efficient reductions to modal logic \textsf{K}

Uses Software

• CUDD

Cites Work

• A near-optimal method for reasoning about action
• A guide to completeness and complexity for modal logics of knowledge and belief
• Symbolic model checking: \(10^{20}\) states and beyond
• The polynomial-time hierarchy
• The proof complexity of analytic and clausal tableaux
• Compute-intensive methods in artificial intelligence
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• NuSMV: A new symbolic model checker
• Resolution for quantified Boolean formulas
• Knowledge and common knowledge in a distributed environment
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Hardware Specification with Temporal Logic: An Example
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Practical reasoning for very expressive description logics
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving

This page was built for publication: BDD-based decision procedures for the modal logic K ★