An essay in combinatory dynamic logic
type: Item
instance of: scholarly article
title: An essay in combinatory dynamic logic
zbMATH Open document ID: 0732.03021
DOI: 10.1016/0890-5401(91)90026-X
author: Solomon Passy
author: Tinko Tinchev
published in: Information and Computation
publication date: 1991-01-01T00:00:00Z
review text: The present extensive paper analyses Combinatory Propositional Dynamic Logic (CPDL) as a fusion of two ideas in the authors' Ph. D. theses: names in modal logic (S. Passy, 1984), and \(\omega\)-axiomatics in dynamic logic (T. Tinchev, 1986). The CPDL language is defined as follows: let \(\Sigma\), \(\Phi_ 0\) and \(\Pi_ 0\) be three countably infinite and pairwise disjoint alphabets, labelled, respectively, as names (or constants), atomic propositions, and atomic programs. The letter \(\nu \not\in \Sigma \cup \Phi_ 0\cup \Pi_ 0\) is called the universe program (or modality). The language of CPDL consists of formulae and programs, inductively defined by: (i) The elements of \(\Sigma \cup \Phi_ 0\) are formulae. The elements of \(\Pi_ 0\cup \{\nu \}\) are programs; (ii) If A, B are formulae, and \(\alpha\), \(\beta\) are programs, then: \(\neg A\), \(A\vee B\), \(<\alpha >A\) are formulae, and \(\alpha\) ;\(\beta\), \(\alpha\cup \beta\), \(\alpha^*\), A? are programs. For \(CPDL^{\cap}\) there is added the clause ``\(\alpha\cap \beta\) is a program''. After an explanatory Prologue, discussing the reasons and purposes of the paper, Chapter 1 gives a fairly detailed approach to CPDL, easily extendable to \(CPDL^{\cap}\). Sections 1-6 contain: the relation to Scott's isomorphism theorem, CPDL axiomatization and proof theory, soundness and completeness for simple extensions of CPDL and \(CPDL^{\cap}\), finitary axiomatization, the finite model property and hence decidability for CPDL. Chapter 2 discusses some interesting extensions of CPDL: Section 2 is motivated by some definitional extensions which are traditionally in the scope of dynamic and modal logics. Section 3 deals with some extensions treating infinity. In Section 4, two exotic extensions of CPDL, admitting a choice function in the models, are proposed. Section 5 discusses CPDL extensions towards polyadic and multi-ary CPDL theory. In Section 6 the authors prove results on the high undecidability of an importan…
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 4210115
zbMATH Keywords: Combinatory Propositional Dynamic Logic
zbMATH Keywords: soundness
zbMATH Keywords: completeness
zbMATH Keywords: extensions of CPDL
zbMATH Keywords: finitary axiomatization
zbMATH Keywords: finite model property
zbMATH Keywords: decidability
zbMATH Keywords: choice function
zbMATH Keywords: quantification
zbMATH Keywords: Stone representation theorem for combinatory dynamic algebras
reviewed by: Neculai Curteanu
MaRDI profile type: Publication
cites work: A complete logic for reasoning about programs via nonstandard model theory. II
cites work: Deterministic propositional dynamic logic: finite models, complexity, and completeness
cites work: Q4194934
cites work: Q4342096
cites work: Nominal tense logic
cites work: An approach to tense logic1
cites work: Q4342093
cites work: Q3748269
cites work: Q3781738
cites work: DAL -- a logic for data analysis
cites work: Graded modalities. I
cites work: Propositional quantifiers in modal logic1
cites work: Normal forms in modal logic
cites work: Investigations in modal and tense logics with applications to problems in philosophy and linguistics
cites work: Q3669373
cites work: Handbook of philosophical logic. Volume II: Extensions of classical logic
cites work: Determinism and looping in combinatory PDL
cites work: Q4694250
cites work: Q3478385
cites work: The unaxiomatizability of a quantified intensional logic
cites work: Q4342097
cites work: Axiomatising the logic of computer programming
cites work: Q3773852
cites work: Q4088789
cites work: Modal definability in enriched languages
cites work: Using the Universal Modality: Gains and Questions
cites work: Q3749041
cites work: The propositional dynamic logic of deterministic, well-structured programs
cites work: First-order dynamic logic
cites work: Recurring Dominoes: Making the Highly Undecidable Highly Understandable
cites work: Inaccessible worlds
cites work: The modal logic of `all and only'
cites work: Boolean Algebras with Operators. Part I
cites work: An elementary proof of the completeness of PDL
cites work: A completeness theorem in modal logic
cites work: Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
cites work: Q5572288
cites work: Q3919070
cites work: Q3957925
cites work: Q3792662
cites work: Descriptively complete process logic
cites work: Q3922159
cites work: Q3326827
cites work: PDL with data constants
cites work: Q3699665
cites work: Concurrent dynamic logic
cites work: Q3475251
cites work: Modality and quantification in S5
cites work: Q5556395
cites work: Q5596205
cites work: Q3744151
cites work: Infinitary propositional normal modal logic
cites work: Q5734410
cites work: Q5573961

An essay in combinatory dynamic logic (cites work)
cites work: An essay in combinatory dynamic logic

An essay in combinatory dynamic logic (cites work)
cites work: Q4694253

An essay in combinatory dynamic logic (cites work)
cites work: Q5596237

An essay in combinatory dynamic logic (cites work)
cites work: Q5551146

An essay in combinatory dynamic logic (cites work)
cites work: Q4068699

An essay in combinatory dynamic logic (cites work)
cites work: Two-dimensional modal logic

An essay in combinatory dynamic logic (cites work)
cites work: Q5537599

An essay in combinatory dynamic logic (cites work)
cites work: Q3322087

An essay in combinatory dynamic logic (cites work)
cites work: Q5184384

An essay in combinatory dynamic logic (cites work)
cites work: Q4039666

An essay in combinatory dynamic logic (cites work)
cites work: Propositional dynamic logic of looping and converse is elementarily decidable

An essay in combinatory dynamic logic (cites work)
cites work: Q5586318

An essay in combinatory dynamic logic (cites work)
cites work: Q3735691

An essay in combinatory dynamic logic (cites work)
cites work: Propositional dynamic logic with local assignments

An essay in combinatory dynamic logic (cites work)
cites work: Q3318100

An essay in combinatory dynamic logic (full work available at URL)
full work available at URL: 0890-5401(91)90026-x

An essay in combinatory dynamic logic (OpenAlex ID)
OpenAlex ID: W2064773636