Logic for Computer Science: Foundations of Automatic Theorem Proving (Harper & Row computer science and technology series) [Hardcover]

Jean Gallier (Author)

Book Description

Series: Harper & Row computer science and technology series | Publication Date: January 1986

Covers the mathematical logic necessary to computer science, emphasizing algorithmic methods for solving proofs. Treatment is self-contained, with all required mathematics contained in Chapter 2 and the appendix. Provides readable, inductive definitions and offers a unified framework using Getzen systems. Offers unique coverage of congruence, and contains an entire chapter devoted to SLD resolution and logic programming (PROLOG). Includes applications to artificial intelligence. Each chapter contains worked examples, programming assignments, problems graded according to difficulty, and historical remarks and suggestions for further reading.

--This text refers to an out of print or unavailable edition of this title.

Product Details

• Hardcover: 528 pages
• Publisher: Longman Higher Education (January 1986)
• Language: English
• ISBN-10: 0060422254
• ISBN-13: 978-0060422257
• Product Dimensions: 9.4 x 6.1 x 1.1 inches
• Shipping Weight: 1.8 pounds
• Average Customer Review: 4.7 out of 5 stars  See all reviews (3 customer reviews)
• Amazon Best Sellers Rank: #2,229,420 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews

4 of 5 people found the following review helpful:

5.0 out of 5 stars Very well written, October 19, 2001

By 

Todd Ebert (Long Beach California) - See all my reviews

This review is from: Logic for Computer Science: Foundations of Automatic Theorem-Proving (Harper & Row Computer Science and Technology Series) (Hardcover)

One of the better books written on automated theorem proving.
The author gives a very clear and lucid treatment of areas such
as propositional and first-order logic, resolution, proof theory
(including Gentzen's cut-elimination theorem), logic programming, and typed logic. This book represents an ideal place to begin for anyone who is interested in developing a deep understanding of the foundations of automated reasoning. Careful detail is given towards Gentzen's tableaux methods for obtaining structural proofs, and the other takes great pains to provide rigorous proofs of the results.

4.0 out of 5 stars A long, difficult but well-written and out of print logic textbook, September 13, 2011

By 

Scott (Dubuque, IA) - See all my reviews

Amazon Verified Purchase

This review is from: Logic for Computer Science: Foundations of Automatic Theorem Proving (Paperback)

INTRODUCTION-PDF AVAILABLE
My first sight of this book was at author professor Jean Gallier's web page for it, at which the whole book in a 2003 revision could be downloaded as a PDF. I did that on Sun 18Oct09 during some kind of logical Google search. Gallier is a professor of CIS / Computer and Information Science at the University of Pennsylvania in Philadelphia and has an interesting faculty web site, which includes some of his PDF papers and family photos, as well as the link to the PDF of this book.

ABOUT THE BOOK PDF
That is a 534 page PDF with lots of front matter increased for the 2003 edition. There are 10 chapters, but only most to all of chapters 3, 5, 6, 7 and 10 have any recommended use by Gallier in teaching courses or seminars from the book. Notably none of chapter 4 on propositional resolution or chapter 8 on first-order resolution or chapter 9 on SLD resolution and logic programming are in the recommended teaching base. A majority of this book concerns various 'Gentzen systems' as ways of doing its proof theoretical tasks. For me those are an intensely opaque way of doing logic.

PRINTING THE PDF
I printed chapters 2 thru 5 on Sat 2Apr11 after having printed and reviewed all the front matter thru short chapter 1 a few months earlier, and ended up grouping the pages of the printouts with awkward steel spring clips. That is one of the problems endemic to printing long PDF files. End of chapter 5 is p. 255 of the book.

DOVER TO PUBLISH IT OR NOT / BOUGHT TWO USED HARDCOPIES
On Tue 30Nov10 I emailed the link to the 2003 PDF to Dover Publications under the idea that maybe they would be willing and able to reprint this book as a fairly inexpensive Dover edition. By Aug11, it appeared and it turns out correctly that Dover would not be reprinting this book, and I located a fairly pricey 'very good condition' used paperback of this book thru Amazon at a place in Maryland. I ordered that book and received it on Mon 29Aug11. This book is a 1987 Wiley paperback edition in terrific condition, so it is more handy for possible reading to have this bound hardcopy available than just the PDF. In late Sep11, I also ordered a less expensive 'very good condition' used hardcover version thru Amazon from a place in Cambridge, MA, the home of both MIT and Harvard. That hardcover is a 1996 copy-on-demand photocopy for the University of Mass. Boston library with thousands of minor copying artifacts, so live and learn. Still being easily and fully readable and with a super robust cover are in that photcopy's favor in spite of those defects.

CONCLUSION
I do find this book to be a highly difficult but fascinating reference text on general Gentzen style proof-theoretical logic, but without much actual automated proof content. A link to a hardcore general proof theory textbook I own: Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science)

GENERAL CONTENTS
1 Introduction / 2 Mathematical Preliminaries / 3 Propositional Logic / 4 Resolution in Propositional Logic / 5 First-Order Logic / 6 Gentzen's Cut Elimination Theorem and Applications / 7 Gentzen's Sharpened Hauptsatz; Herbrand's Theorem / 8 Resolution in First-Order Logic / 9 SLD-Resolution and Logic Programming (Prolog) / 10 Many-Sorted First-Order Logic / Appendix / References / Index of Symbols / Index of Definitions / Subject Index

3 of 5 people found the following review helpful:

5.0 out of 5 stars i luv it!, April 13, 1999

By A Customer

This review is from: Logic for Computer Science: Foundations of Automatic Theorem-Proving (Harper & Row Computer Science and Technology Series) (Hardcover)

this book is excellent and reading it one can clearly see galliers geometric insight influenced by the great french mathematicians cartan and serre! -kurt reillag