Tableaux methods for propositional dynamic logics with separating parallel composition

DOI10.1007/978-3-319-21401-6_37MaRDI QIDQ3454121zbMATH OpenOpenAlexFDO

Authors Philippe Balbiani, Joseph Boudou

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-21401-6_37

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• A practical decision method for propositional dynamic logic (preliminary report)
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Propositional dynamic logic with storing, recovering and parallel composition
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• scientific article; zbMATH DE number 4068839

Cites work

• A description logic with transitive and inverse roles and role hierarchies
• A modal BI logic for dynamic resource properties
• A near-optimal method for reasoning about action
• Algebra and logic for resource-based systems modelling
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Computer Science Logic
• Concurrent dynamic logic
• Decidable and undecidable logics with a binary modality
• scientific article; zbMATH DE number 3983144 (Why is no real title available?)
• scientific article; zbMATH DE number 3624763 (Why is no real title available?)
• scientific article; zbMATH DE number 6863850 (Why is no real title available?)
• Iteration-free \(\mathrm{PDL}\) with storing, recovering and parallel composition: a complete axiomatization
• Propositional dynamic logic of regular programs
• Propositional dynamic logic with storing, recovering and parallel composition
• Reasoning about sequences of memory states
• Separation logics and modalities: a survey
• The semantics and proof theory of the logic of bunched implications

Cited in

(8)

• Bisimilar and logically equivalent programs in PDL with parallel operator
• Tableaux for constructive concurrent dynamic logic
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Exponential-size model property for PDL with separating parallel composition
• Tableaux for Reasoning about Atomic Updates
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• Propositional dynamic logic with storing, recovering and parallel composition
• Shortcuts and dynamic marking in the tableau method for adaptive logics

This page was built for publication: Tableaux methods for propositional dynamic logics with separating parallel composition

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