author : Robert Goldblatt

Part One sets out the basic theory of normal modal and temporal propositional logics, covering the canonical model construction used for completeness proofs, and the filtration method of constructing finite models to prove decidability results and completeness theorems. New material covers first-order definability, canonicity, and undecidability.

Part Two applies this theory to logics of discrete, dense, and continuous time; to the temporal logic of henceforth, next, and until, as used in the study of concurrent programs; and to dynamic logic. For this edition, the temporal logic of concurrency is extended to branching time, studying a system of Computational Tree Logic that formalises reasoning about behaviour along different branches of the tree of possible future states. Dynamic logic is extended to the case of concurrency, introducing a connective for parallel execution of commands and requiring a new theory of canonical models and filtrations that has not been studied previously.

Part Three is devoted to quantificational dynamic logic, and focuses on the relationship between the computational process of assignment to a variable, and the syntactic process of substitution for a variable. A completeness theorem is obtained for an infinitary proof theory.

The text contains numerous exercises, and has been specifically designed to be effective for use in the classroom.