An on-the-fly tableau-based decision procedure for PDL-satisfiability

DOI10.1016/J.ENTCS.2009.02.036MaRDI QIDQ4982121zbMATH OpenOpenAlexFDO

Authors Pietro Abate, Rajeev Goré, 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 reasoningdecision procedurepropositional dynamic logictableau calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• A practical decision method for propositional dynamic logic (preliminary report)
• Optimal and cut-free tableaux for propositional dynamic logic with converse
• Clausal tableaux for hybrid PDL
• A tableau-based decision procedure for CTL^*

Cites work

• A near-optimal method for reasoning about action
• About cut elimination for logics of common knowledge
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• Cut-free common knowledge
• Decision procedures and expressiveness in the temporal logic of branching time
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 67500 (Why is no real title available?)
• One-Pass Tableaux for Computation Tree Logic
• Optimizing description logic subsumption
• Propositional dynamic logic of regular programs
• Tableau-based model checking in the propositional mu-calculus
• Temporal logic can be more expressive
• The temporal logic of branching time

Cited in

(15)

• Tableaux with partial caching for hybrid PDL with satisfaction statements
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• A goal-directed decision procedure for hybrid PDL
• Clausal tableaux for hybrid PDL
• TATL: Implementation of ATL Tableau-Based Decision Procedure
• Checking consistency of an ABox w.r.t. global assumptions in PDL
• Implementing a relational theorem prover for modal logic K
• A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
• ExpTime tableaux with global caching for graded propositional dynamic logic
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• A practical decision method for propositional dynamic logic (preliminary report)
• Optimal and cut-free tableaux for propositional dynamic logic with converse
• Terminating Tableaux for Hybrid Logic with Eventualities
• SAT meets tableaux for linear temporal logic satisfiability

This page was built for publication: An on-the-fly tableau-based decision procedure for PDL-satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4982121)