Florian Bruse (University of Kassel) |
Daniel Kernberger (University of Kassel) |
Martin Lange (University of Kassel) |
We study the axiomatisability of the iteration-free fragment of Propositional Dynamic Logic with Intersection and Tests. The combination of program composition, intersection and tests makes its proof-theory rather difficult. We develop a normal form for formulae which minimises the interaction between these operators, as well as a refined canonical model construction. From these we derive an axiom system and a proof of its strong completeness. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.226.9 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |