Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse

DOI10.1007/978-3-642-14203-1_20zbMath1291.68345OpenAlexW2161218164MaRDI QIDQ5747763

Rajeev Goré, Florian Widmann

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_20

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Related Items (8)

CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT ⋮ ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ Verified Decision Procedures for Modal Logics. ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ Clausal Tableaux for Hybrid PDL ⋮ ExpTime tableau decision procedures for regular grammar logics with converse ⋮ A goal-directed decision procedure for hybrid PDL

Uses Software

• OCaml

Cites Work

• Unnamed Item
• Automata-theoretic techniques for modal logics of programs
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Sound Global State Caching for ALC with Inverse Roles
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• KI 2003: Advances in Artificial Intelligence

This page was built for publication: Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse