A Canonical Model Construction for Iteration-Free PDL with Intersection
Logic in Computer Science
2016-09-15 v1
Abstract
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.
Keywords
Cite
@article{arxiv.1609.04093,
title = {A Canonical Model Construction for Iteration-Free PDL with Intersection},
author = {Florian Bruse and Daniel Kernberger and Martin Lange},
journal= {arXiv preprint arXiv:1609.04093},
year = {2016}
}
Comments
In Proceedings GandALF 2016, arXiv:1609.03648