A Canonical Model Construction for Iteration-Free PDL with Intersection

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
id doaj-c763092832b942648402cd40e32bffac
record_format Article
spelling doaj-c763092832b942648402cd40e32bffac2020-11-25T00:09:28ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-09-01226Proc. GandALF 201612013410.4204/EPTCS.226.9:20A Canonical Model Construction for Iteration-Free PDL with IntersectionFlorian Bruse0Daniel Kernberger1Martin Lange2 University of Kassel University of Kassel 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.http://arxiv.org/pdf/1609.04093v1
collection DOAJ
language English
format Article
sources DOAJ
author Florian Bruse
Daniel Kernberger
Martin Lange
spellingShingle Florian Bruse
Daniel Kernberger
Martin Lange
A Canonical Model Construction for Iteration-Free PDL with Intersection
Electronic Proceedings in Theoretical Computer Science
author_facet Florian Bruse
Daniel Kernberger
Martin Lange
author_sort Florian Bruse
title A Canonical Model Construction for Iteration-Free PDL with Intersection
title_short A Canonical Model Construction for Iteration-Free PDL with Intersection
title_full A Canonical Model Construction for Iteration-Free PDL with Intersection
title_fullStr A Canonical Model Construction for Iteration-Free PDL with Intersection
title_full_unstemmed A Canonical Model Construction for Iteration-Free PDL with Intersection
title_sort canonical model construction for iteration-free pdl with intersection
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2016-09-01
description 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.
url http://arxiv.org/pdf/1609.04093v1
work_keys_str_mv AT florianbruse acanonicalmodelconstructionforiterationfreepdlwithintersection
AT danielkernberger acanonicalmodelconstructionforiterationfreepdlwithintersection
AT martinlange acanonicalmodelconstructionforiterationfreepdlwithintersection
AT florianbruse canonicalmodelconstructionforiterationfreepdlwithintersection
AT danielkernberger canonicalmodelconstructionforiterationfreepdlwithintersection
AT martinlange canonicalmodelconstructionforiterationfreepdlwithintersection
_version_ 1725411783022215168

Similar Items