
This paper considers propositional modal logics with a bundle of modalities. Each modality is intended intuitively to be the input-output relationship of a program, yielding a binary relation of the so-called Kripke sort formally. After claiming the completeness theorem, the author considers within this framework how we should characterize program connectives of algorithmic logic such as ''either \(\alpha\) or \(\beta\) '' syntactially, only to leave the characterization of the elusive connective ''while P do \(\alpha\) '' open.
algorithmic logic, Modal logic (including the logic of norms), Abstract data types; algebraic specification, modal logic, Kripke semantics
algorithmic logic, Modal logic (including the logic of norms), Abstract data types; algebraic specification, modal logic, Kripke semantics
