Customer Reviews

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

5 star:		(2)
4 star:		(1)
3 star:		(0)
2 star:		(0)
1 star:		(0)

 

 

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.

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

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