Logic for computer science : foundations of automatic theorem proving / Jean H. Gallier

The book is an intensive introduction to the study of proof systems and algorithmic methods for constructing proofs in mathematical logic. Some outstanding but fruitful features characterize this wonderful textbook: the use of Gentzen systems, a justification of the resolution method via a translation from a Gentzen system, a representation of SLD-resolution and of the foundations of PROLOG, fast decision procedures based on congruence closures. The author's option for Gentzen systems is very promising both from pedagogical and scientific point of view: Gentzen-style rules reflect directly the semantics of logical connectives, naturally lead to mechanical proof procedures, have duality built in, the completeness theorem is naturally obtained, etc. For valid formulas, proof trees are constructed by a search procedure described in a pseudo-PASCAL program. A proof procedure for first-order logic with equality can be incrementally developed, starting with the propositional case. More generally, the option for Gentzen style is mainly the option for rigorous constructivism and provability of the logical systems. A brief description of the contents: Chapter 2 is a mathematical introduction necessary to computer science and logical notions. Chapter 3 introduces Gentzen systems for propositional logic. The completeness theorem is proved. Introducing infinite sequents, the extended completeness theorem and the compact theorem are obtained. The complexity classes P, NP and the concept of NP-completeness are discussed. In Chapter 4 the completeness of resolution is obtained by defining a special Gentzen system and an algorithm is given for converting proofs in the special Gentzen systems into resolution refutations. In Chapter 5 the Gentzen systems are extended to deal with first-order logic. It is shown that every Hintikka set is satisfiable in a model whose domain is a term algebra. This result is used to derive the main theorems of first-order logic: completeness, compactness, model existence, and Löwenheim-Skolem theorems. Chapter 6 is devoted to Gentzen's cut elimination theorem (Hauptsatz) and some of its applications. It contains more technical results, relating and obtaining new and classical results. In Chapter 7, Gentzen's sharpened Hauptsatz is proved constructively using proof transformation techniques. Constructive versions of Herbrand's theorem are proved as well as Andrew's version of the Skolem-Herbrand-Gödel theorem. Chapter 8 extends the resolution method to first order logic, represents a Robinson-type recursive unification algorithm and the completeness of first order resolution. Chapter 9 is devoted to SLD- resolution and the foundations of PROLOG. A model-theoretic semantics for logic programs is defined. The completeness of SLD-resolution is shown by translating proofs in a certain Gentzen system into SLD-refuations. SLD- resolution is proved to be a sound and complete computational procedure for logic programs. Chapter 10 introduces many-sorted first-order logic and its semantics based on many-sorted algebras. Fast decision procedures for deciding whether a quantifier-free formula is valid are given using the congruence closure method. A quite special mention for the set of problems at the end of every chapter, completing the theoretical aspects and realizing a very active reading. A (text)book of reference by its rigour, constructivism and density. A deep satisfaction for (mathematical formation) students and researchers in (computer science) logic. (Zentralblatt)