@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
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\ {\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. }
}