scientific article; zbMATH DE number 139632

Authors Tinko Tinchev, Dimiter Vakarelov

Publication date 28 March 1993

completeness dynamic algebras fixed-point semantics generalization of PDL infinitary axiomatization recursion operator on programs

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Other algebras related to logic (03G25) Semantics in the theory of computing (68Q55)

Review text

[For the entire collection see Zbl 0745.00057.] In this paper we introduce a generalization of PDL and dynamic algebras in which the operation of iteration procedure \(\alpha^*\) is replaced by a more complex recursion operator on programs \(\Gamma_ \omega(\alpha_ 1,\dots,\alpha_ n)\). An arithmetical axiomatization of a first-order dynamic logic with recursive procedures is given by \textit{D. Harel} [First-order dynamic logic (Lect. Notes Comput. Sci. 68) (1979; Zbl 0403.03024)] (Harel calls his logic a context-free dynamic logic --- CFDL). In this paper we consider a kind of a propositional version of CFDL and give for it an infinitary axiomatization in the style of \textit{G. Mirkowska} [Lect. Notes Comput. Sci. 125, 23-101 (1981; Zbl 0487.03012)] and \textit{R. Goldblatt} [Axiomatising the logic of computer programming (Lect. Notes Comput. Sci. 130) (1982; Zbl 0474.68045)] and a completeness theorem with respect to a fixed-point semantics. For that purpose we first introduce the notion of \(\Gamma_ \omega\)-dynamic algebra and give an analog of the Stone set- representation theorem for some class of such algebras.

Recommendations

Cited in

(17)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4029612)