## An essay in combinatory dynamic logic

S. Passy and T. Tinchev. An essay in combinatory dynamic logic. Information and Computation, 93:263–332, 1991.

#### Abstract:

The language of combinatory propositional dynamic logic (CPDL) is an enrichment of PDL by the universal modality and so-called names. The universal modality is an S5 modality with the extra requirement that the relation is the total relation on every frame; and the names are like proposition variables but are true at exactly one point. These two ingredients in CPDL remedy some deficiencies of PDL that result from its restricted expressive power. In addition to the axioms and rules that follow from the given interpretation the authors add the following rule: $$(\rm cov)\quad \rm If \vdash[\gamma]c \rm for all names c&nbsp;\rm then \vdash[\gamma]0.$$ Given that we have countably many names, only countable frames satisfy (cov), and frames are CPDL-equivalent if and only if they are isomorphic. The essay starts with a historical chapter on PDL and CPDL that is worth reading even if one is not interested in the special topic of this paper. We are presented with the considerations that have led to the particular choice of extension of PDL. Then follows a chapter on "pure" CPDL, its proof theory and semantics. The third part takes us through a maze of possible ways to enrich or strengthen CPDL, starting with the logic of deterministic atomic programs, continuing with definitional extensions such as adding equality statements for programs or negations and converses; and concluding with additions to handle infinities in computations. The fourth and final chapter discusses the effects of adding quantifiers over names.

@ARTICLE{passy91,
author = {S. Passy and T. Tinchev},
title = {An essay in combinatory dynamic logic},
journal = {Information and Computation},
year = {1991},
volume = {93},
pages = {263-332},
abstract = {
The language of combinatory propositional dynamic logic (CPDL) is
an enrichment of PDL by the universal modality and so-called names.
The universal modality is an S5 modality with the extra requirement
that the relation is the total relation on every frame; and the names
are like proposition variables but are true at exactly one point.
These two ingredients in CPDL remedy some deficiencies of PDL that
result from its restricted expressive power. In addition to the axioms
the following rule: $$({\rm cov})\quad {\rm If} \vdash[\gamma]c {\rm for all names} c\ {\rm then} \vdash[\gamma]0.$$ Given that we have
countably many names, only countable frames satisfy (cov), and frames
are CPDL-equivalent if and only if they are isomorphic.
The essay starts with a historical chapter on PDL and CPDL that is
worth reading even if one is not interested in the special topic
of this paper. We are presented with the considerations that have
led to the particular choice of extension of PDL. Then follows a
chapter on "pure" CPDL, its proof theory and semantics. The third
part takes us through a maze of possible ways to enrich or strengthen
CPDL, starting with the logic of deterministic atomic programs, continuing
with definitional extensions such as adding equality statements for
programs or negations and converses; and concluding with additions
to handle infinities in computations. The fourth and final chapter
discusses the effects of adding quantifiers over names. }
}


Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33

Hybrid Logics
Resources