Handbook of logic in computer science. Vol. 2: Background: Computational structures. (English) Zbl 0777.68001

Artificial Intelligence and Logic Programming. Oxford: Clarendon Press. X, 571 p. (1992).
This articles of this volume will not be reviewed individually.
The text is one volume in a series the goal of which is to survey the applications of logic in computer science. The topics in this volume on computational structures are term rewriting systems, lambda calculi, algorithmic logics, theorem provers, and modal and temporal logics.
Term rewriting systems are probably best known through their most famous example, the lambda calculus, in which a computation can be viewed as proceeding by successive application of the rewrite rules. The point of view taken here is that of starting very abstractly, with an abstract reduction system being taken as a set with binary relations, called reduction relations. Ever more structure is then assumed on this system, with a corresponding increase in the properties that can be proven about it (such as weak or strong normalization, or Church-Rosser). The systems considered include term rewriting systems, in which the rewrite rules operate on the terms of a first-order language, orthogonal TRSs (elsewhere known as non-ambiguous and left-linear TRSs), and conditional TRSs. Some of the topics discussed are proving termination via recursive path orderings, and Knuth-Bendix completion.
The chapter on the lambda calculus discusses three versions: type-free, Curry typing, and Church typing. The highlights of the section on the type-free system are the representation of the natural numbers, the proof that all recursive functions are representable, Church-Rosser, and a discussion on normalization. Within the typed lambda calculus, a distinction is made between Curry typing, or implicit typing as in ML, and Church typing, or explicit typing as in Pascal. Several systems within each paradigm are introduced, and the Curry-Howard or propositions-as-types interpretation is presented for the Church systems.
Regarding algorithmic logic, the traditional view of a logic is as a consequence relation \(\vdash\). Here a logic is taken as a consequence relation along with an algorithm for deciding whether \(\mathbb{P}\vdash A\). Starting with a decision algorithm for intuitionistic logic with implication, the author examines natural variations on the algorithm, often motivated by a desire for optimizing the algorithm’s performance, and produces algorithmic versions of classical and of linear logic, as well as others. It is also discussed how to extend these algorithms to more expressive systems, such as those with more boolean connectives and, more importantly, quantifiers.
The topic of theorem provers is addressed by a case study. The prover chosen was Folderol, described as a toy theorem prover intended to illustrate the issues involved in designing a theorem prover. Some other well-known provers are discussed, such as the Boyer/Moore theorem prover, Automath, LCF, and Isabelle.
The computational setting for the discussion on modal and temporal logics is that of transition systems, which are a model for computer systems. A transition system consists of a set of states, and a set of transitions, each of which is, formally, a binary relation on the set of states, and, less formally, a procedure leading from one state to another. Transitions systems are used here as models of modal and temporal logics. Variants of modal and temporal logic are introduced, most prominently the modal and temporal mu-calculi, where a mu-calculus is one which includes a least fixed point operator. Other topics addressed are the expressive power of the chosen modal and temporal operators, and the soundness and completeness of axiom systems.


68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science
68Q42 Grammars and rewriting systems
03D03 Thue and Post systems, etc.
03B40 Combinatory logic and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B70 Logic in computer science
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)


LCF; Isabelle