Tableaux and algorithms for Propositional Dynamic Logic with Converse

DOI10.1007/3-540-61511-3_117MaRDI QIDQ4647551zbMATH OpenOpenAlexFDO

Authors Giuseppe De Giacomo, Fabio Massacci

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

description logicmodal logicopen branchpropositional dynamic logicpropositional letter

Mathematics Subject Classification ID

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

Recommendations

• Optimal and cut-free tableaux for propositional dynamic logic with converse
• Tableaux for constructive concurrent dynamic logic
• Tableaux methods for propositional dynamic logics with separating parallel composition
• scientific article; zbMATH DE number 7713505
• Tableaux for a combination of propositional dynamic logic and epistemic logic with interactions
• TABLEAUX: A general theorem prover for modal logics
• Tableau calculi for logic programs under answer set semantics
• scientific article; zbMATH DE number 1361525
• scientific article; zbMATH DE number 3968565
• Tableaux with Dynamic Filtration for Layered Modal Logics

Cites work

• A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
• A guide to completeness and complexity for modal logics of knowledge and belief
• A modal perspective on the computational complexity of attribute value grammar
• A near-optimal method for reasoning about action
• A practical decision method for propositional dynamic logic (preliminary report)
• Automata-theoretic techniques for modal logics of programs
• scientific article; zbMATH DE number 67503 (Why is no real title available?)
• scientific article; zbMATH DE number 1142324 (Why is no real title available?)
• Local model checking in the modal mu-calculus
• Modal Logic, Transition Systems and Processes
• Proof methods for modal and intuitionistic logics
• Propositional dynamic logic of regular programs
• Strongly analytic tableaux for normal modal logics
• The KL-ONE family

Cited in

(14)

• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Eliminating ``converse from converse PDL
• Tableaux for constructive concurrent dynamic logic
• Tableaux methods for propositional dynamic logics with separating parallel composition
• Tableaux for single-agent epistemic PDL with perfect recall and no miracles
• A Tableaux System for Deontic Action Logic
• scientific article; zbMATH DE number 3974280 (Why is no real title available?)
• Tableaux methods for access control in distributed systems
• A Tableau Calculus for Regular Grammar Logics with Converse
• scientific article; zbMATH DE number 4197949 (Why is no real title available?)
• Optimal and cut-free tableaux for propositional dynamic logic with converse
• Shortcuts and dynamic marking in the tableau method for adaptive logics
• scientific article; zbMATH DE number 7713505 (Why is no real title available?)
• On the complexity of the two-variable guarded fragment with transitive guards

This page was built for publication: Tableaux and algorithms for Propositional Dynamic Logic with Converse

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