Logic For Computer Science - Foundations of Automatic Theorem Proving

An introduction to mathematical logic, with an emphasis on proof theory and procedures for constructing formal proofs of formulae algorithmically.

Publication date: 18 Jun 2015

ISBN-10: 0486780821

ISBN-13: 9780486780825

Paperback: 534 pages

Views: 26,702

Type: Textbook

Publisher: Dover Publications

Post time: 09 Sep 2006 08:58:47

Logic For Computer Science - Foundations of Automatic Theorem Proving

An introduction to mathematical logic, with an emphasis on proof theory and procedures for constructing formal proofs of formulae algorithmically.
Tag(s): Logic Programming Proofs
Publication date: 18 Jun 2015
ISBN-10: 0486780821
ISBN-13: 9780486780825
Paperback: 534 pages
Views: 26,702
Document Type: Textbook
Publisher: Dover Publications
Post time: 09 Sep 2006 08:58:47
Terms and Conditions:

Book Excerpts:
Jean Gallier wrote:This book is intended as an introduction to mathematical logic, with an emphasis on proof theory and procedures for constructing formal proofs of formulae algorithmically.

Since the main emphasis of the text is on the study of proof systems and algorithmic methods for constructing proofs, it contains some features rarely found in other texts on logic. Four of these features are:

1. The use of Gentzen Systems;
2. A Justification of the Resolution method via a translation from a Gentzen System;
3. A presentation of SLD-resolution and a presentation of the foundations of PROLOG;
4. Fast decisions procedures based on congruence closures.

Even though the main emphasis of the book is on the design of procedures for constructing formal proofs, the treatment of the semantics is perfectly rigorous. The following paradigm has been followed: Having defined the syntax of the language, it is shown that the set of well-formed formulae is a freely generated inductive set. This is an important point, which is often glossed over. Then, the concepts of satisfaction and validity are defined by recursion over the freely generated inductive set (using the 'unique homomorphic extension theorem', which can be rigorously justified). Finally, the proof theory is developped, and procedures for constructing proofs are given. Particular attention is given to the complexity of such procedures.

Intended Audience:

This book is designed primarily for computer scientists, and more generally, for mathematically inclined readers interested in the formalization of proofs, and the foundations of automatic theorem-proving.

This book is written at the level appropriate to senior undergraduate and first year graduate students in computer science, or mathematics. The prerequesites are the equivalent of undergraduate-level courses in either set theory, abstract algebra, or discrete structures. All the mathematical background necessary for the text itself is contained in Chapter 2, and in the Appendix. Some of the most difficult exercises may require deeper knowledge of abstract algebra.

Review(s):