Tableaux and algorithms for Propositional Dynamic Logic with Converse

DOI10.1007/3-540-61511-3_117zbMath1412.68216OpenAlexW1555569636MaRDI QIDQ4647551

Fabio Massacci, Giuseppe De Giacomo

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_117

zbMATH Keywords

modal logicdescription logicpropositional dynamic logicopen branchpropositional letter

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Logic in computer science (03B70)

Related Items

On the complexity of the two-variable guarded fragment with transitive guards ⋮ A Tableaux System for Deontic Action Logic ⋮ Tableaux methods for access control in distributed systems ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL.

Cites Work

• Unnamed Item
• Unnamed Item
• Proof methods for modal and intuitionistic logics
• Automata-theoretic techniques for modal logics of programs
• A near-optimal method for reasoning about action
• Local model checking in the modal mu-calculus
• A guide to completeness and complexity for modal logics of knowledge and belief
• The KL-ONE family
• Propositional dynamic logic of regular programs
• A modal perspective on the computational complexity of attribute value grammar
• A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
• Modal Logic, Transition Systems and Processes
• Strongly analytic tableaux for normal modal logics
• A practical decision method for propositional dynamic logic (Preliminary Report)