No label defined (Q4040458)

In Volume I of this treatise (1985; Zbl 0572.68008), the authors have given a presentation of semantics of first-order predicate logic and an introduction to simple theories important for Computer Science, namely, theories of strings, trees, lists and sets. Volume II demonstrates the formal content of proofs in first-order logic by presenting a deductive system based on the tableaux method. At the beginning of the book it is stressed that these deductive systems are ``machine oriented'' or, in other words, are amenable to an implementation in an automatic or interactive computer theorem prover. The book is divided into four parts: I. Well-founded induction, II. Propositional logic, III. Unification and IV. Predicate logic. The second part gives a detailed discussion of deductive tableaux in the propositional case. The third part introduces the theory of expressions and the theory of unification, and presents the proof of the Unification Theorem concerning the Unification Algorithm. The last part of the book presents the logical rules concerning quantifiers and Skolem functions. deductive tableaux for predicate logic and the general resolution rule are discussed. Some special theories are examined, namely finite theories, finite theories with equality and theories with induction. For this purpose, some results of the first part of the volume are used. The Decidability and Completeness Theorems are shortly described at the end of the book. A selection of recommended readings, Index of symbols and a General Index complete the book. The presentation is oriented to readers that are less mathematically oriented and are more interested in Computer Science. Every part starts with an informal discussion of the main topics and then gives a detailed presentation. The book is recommendable to a reader who has no previous experience with more conventional logic texts. Such a reader may then enjoy the logic environment presented. A mathematically oriented reader may find a 150 pages long introduction to well-founded relations too lengthy and may not feel well with the notation.