Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition

DOI10.1007/978-3-319-21401-6_37zbMath1465.03050OpenAlexW1478819493MaRDI QIDQ3454121

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

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

Related Items (2)

Bisimilar and logically equivalent programs in PDL with parallel operator ⋮ Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

Cites Work

• Reasoning about sequences of memory states
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Decidable and undecidable logics with a binary modality
• The semantics and proof theory of the logic of bunched implications
• A Modal BI Logic for Dynamic Resource Properties
• Algebra and logic for resource-based systems modelling
• Concurrent dynamic logic
• A description logic with transitive and inverse roles and role hierarchies
• Separation logics and modalities: a survey
• Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization
• Propositional Dynamic Logic with Storing, Recovering and Parallel Composition
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Computer Science Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition