A Canonical Model Construction for Iteration-Free PDL with Intersection

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 betwe...

Full description

Bibliographic Details
Main Authors: Florian Bruse, Daniel Kernberger, Martin Lange
Format: Article
Language:English
Published: Open Publishing Association 2016-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1609.04093v1