An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability

DOI10.1007/978-3-642-02959-2_32zbMath1250.03017OpenAlexW2145369884MaRDI QIDQ5191118

Rajeev Goré, Florian Widmann

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1885/54800

zbMATH Keywords

propositional dynamic logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition, ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching, Invariant-free clausal temporal resolution, Tableaux for realizability of safety specifications, Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics, Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse, Terminating Tableaux for Hybrid Logic with Eventualities, ExpTime tableaux with global caching for hybrid PDL, Clausal Tableaux for Hybrid PDL, A logic framework for reasoning with movement based on fuzzy qualitative representation, A goal-directed decision procedure for hybrid PDL

Uses Software

• OCaml

Cites Work

• Unnamed Item
• ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
• Cut-free sequent systems for temporal logic
• Automata-theoretic techniques for modal logics of programs
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• BDD-based decision procedures for the modal logic K ★
• Optimizing description logic subsumption
• An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability