×

Lectures on infinitary logic and logics of programs. Collected by Gianfranco Mascari. (English) Zbl 0597.03016

Quad., Ser. III, Ist. Appl. Calcolo 142, 122 p. (1982).
The goal of these lecture notes is to give the reader an introduction to several logics of programs and the infinitary logic \(L_{\omega_ 1\omega}\). The author begins with an introductory chapter: ”Forward in Boolean algebras”, in which some fundamentals on Boolean algebras used in the context of the logics considered are reminded. Chapter III treats regular program schemes, thus preparing their use in the chapters on program logics. In the remaining chapters (II,IV-VII) the following logics are considered, respectively: ”The infinitary logic \(L_{\omega_ 1\omega}''\); ”Algorithmic logic with quantifiers: a logic of deterministic regular programs”; ”A logic of regular programs”; ”A logic of syntactic interacting stacks”; ”A logic of regular programs with syntactic interacting stacks”. Each of these chapters is divided into the following four parts, respectively: Syntax; Semantics; Proofs; Completeness theorem.

MSC:

03B60 Other nonclassical logic
03C75 Other infinitary logic
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
68-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science
03-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
68-02 Research exposition (monographs, survey articles) pertaining to computer science
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations