An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability

DOI10.1016/j.entcs.2009.02.036zbMath1347.68298MaRDI QIDQ4982121

Rajeev Goré, Pietro Abate, Florian Widmann

Publication date: 23 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.02.036

zbMATH Keywords

automated reasoning; tableau calculus; propositional dynamic logic; decision procedure

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

03B70: Logic in computer science

Related Items

An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability, An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability, Terminating Tableaux for Hybrid Logic with Eventualities, A goal-directed decision procedure for hybrid PDL, Clausal Tableaux for Hybrid PDL, Implementing a relational theorem prover for modal logic

Cites Work

• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• Tableau-based model checking in the propositional mu-calculus
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• About cut elimination for logics of common knowledge
• Decision procedures and expressiveness in the temporal logic of branching time
• Cut-free common knowledge
• Temporal logic can be more expressive
• One-Pass Tableaux for Computation Tree Logic
• Optimizing description logic subsumption
• An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability