A unifying theorem for algebraic semantics and dynamic logics

computational models of programs continuous algebras dynamic algebras first-order axiomatizability first-order definability of classes of models ultraproducts

Mathematics Subject Classification ID

Logic in computer science (03B70) General topics in the theory of software (68N01) Abstract data types; algebraic specification (68Q65)

Review text

Various logics have been proposed and studied for expressing and proving program properties. This paper considers the problem whether the class of models of a logic is first-order definable, yielding a general tool to prove that it is not first-order axiomatizable if it is indeed not. The authors show, by using the technical tool of ultraproducts, that a class of structures which is first-order axiomatizable is bounded in the sense that all iterations stop after a finite number of steps. They apply this idea to continuous algebras, dynamic algebras and general computational models of programs. They deduce as easy corollaries of the main theorem the results of \textit{A. J. Kfoury} and \textit{D. M. Park} [Inf. Control 29, 243-251 (1975; Zbl 0329.68015)] and \textit{B. Courcelle} and \textit{I. Guessarian} [J. Comput. Syst. Sci. 17, 388-413 (1978; Zbl 0392.68009)] and others.

Recommendations

Cites work

Cited in

(6)

This page was built for publication: A unifying theorem for algebraic semantics and dynamic logics

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