Jean H. Gallier - Logic for Computer Science : Foundations of Automatic Theorem Proving

LOGIC FOR COMPUTER SCIENCE

Foundations of Automatic Theorem Proving

SECOND EDITION

Jean H. Gallier

Department of Computer and Information Science University of Pennsylvania

Dover Publications, Inc.

Mineola, New York

Copyright

Copyright 1986, 2015 by Jean H. Gallier

All rights reserved.

Bibliographical Note

This Dover edition, first published in 2015, is an unabridged republication of the revised 2003 online edition of the work originally published by Harper & Row, New York, in 1986. A new Preface to the Dover Edition has been specially prepared for this volume.

Library of Congress Cataloging-in-Publication Data

Gallier, Jean H.

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

pages cm. (Dover books on computer science)

This Dover edition, first published in 2015, is an unabridged republication of the revised 2003 online edition of the work originally published by Harper & Row, New York, in 1986. A new Preface to the Dover Edition has been specially prepared for this volume.

Includes bibliographical references and index.

ISBN-13: 978-0-486-78082-5 (paperback) ISBN-10: 0-486-78082-1 (paperback)

1. Automatic theorem proving. 2. Logic, Symbolic and mathematical. I. Title.

QA76.9.A96G35 2015

511.36028563dc23

2014048078

Manufactured in the United States by Courier Corporation

78082101 2015

www.doverpublications.com

To Anne, my wife,

Mia, Philippe and Sylvie, my children,

and my mother, Simone

Preface (Dover Edition)

Logic for Computer Science, initially published in 1985 has been out of print since 2000. Nevertheless, there has been continued demand for my book, and this prompted me in 2003 to correct all known mistakes and typos and to put a copy available online. I am honored that Dover proposed reprinting a hard copy of my book, and I hope that this will be attractive to readers interested in mathematical sciences and philosophy.

This republication of my book is a slightly revised version of the 1985 edition of my logic book. Many typos and errors have been corrected and the line drawings have been improved. Most mistakes were minor, except for a subtle error in is also false.

In this revised edition, I simply removed all statements about the complexity of the conversion of resolution refutations into proof trees. Hopefully, this part of the book is now correct, as well as the rest of it!

Some parts of the book have now aged, in particular, the parts about PROLOG. Also, thirty years later, I would prefer to present some of the material in a different order and in a different manner. In particular, I would separate more clearly the material on the resolution method () from the more proof-theory oriented material. However, I consider this too big a task and this mildly revised version will have to do (at least, for now!).

Ideally, a number of topics should also be covered, for example, some basics of constructive logic, linear logic, temporal logic and model checking. Again, this is too formidable a task for a single individual and I hope that readers enjoy this new version of my book anyway.

It should be noted that this book is of preTEX vintage. This means that LaTEX was not available at the time this book was written, which implies that I had to write macros (stolen and adapted from D. Knuth blue TEX book) to do chapter headings, etc. Fortunately, Dover converted my TEX files to LaTEX; many thanks for accomplishing this tedious task. Nevertheless, I am grateful to Knuth for producing TEX. Without it, this book would not be alive.

In retrospect, I realize how much I was inspired by, and thus, how much I owe, Gerhard Gentzen, Jacques Herbrand, Stephen Kleene, Gaisi Takeuti, Raymond Smullyan, Peter Andrews and last but not least, Jean-Yves Girard. You have my deepest respect for your seminal and inspiring work and I thank all of you for what you taught me.

Philadelphia, March 2015

Jean Gallier

Preface (1985 Edition)

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.

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.

The book is self contained, and the level corresponds to senior undergraduates and first year graduate students. However, there is enough material for at least a two semester course, and some Chapters () contain material which could form the basis of seminars. It would be helpful, but not indispensable, if the reader has had an undergraduate-level course in set theory and/or modern algebra.

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.

A fruitful way to use this text is to teach PROLOG concurently with the material in the book, and ask the student to implement in PROLOG some of the procedures given in the text, in order to design a simple theorem-prover.

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 developed, and procedures for constructing proofs are given. Particular attention is given to the complexity of such procedures.

In our opinion, the choice of Gentzen systems over other formal systems is pedagogically very advantageous. Gentzen-style rules reflect directly the semantics of the logical connectives, lead naturally to mechanical proof procedures, and have the advantage of having duality built in. Furthermore, in our opinion, Gentzen systems are more convenient than tableaux systems or natural deduction systems for proof-theoretical investigations (cut-free proofs in particular). In three years of teaching, I have found that Gentzen-like systems were very much appreciated by students.

Another good reason for using a formal system inspired from Gentzen (a sequent calculus), is that the completeness theorem is obtained in a natural and simple way. Furthermore, this approach even yields a program (the searchprocedure) for constructing a proof tree for a valid formula. In fact, in our presentation of the completeness theorem (inspired by Kleene, Kleene 1967), the search for a proof tree is described by a program written in pseudo-PASCAL. We also show how a proof procedure for first-order logic with equality can be developed incrementally, starting with the propositional case.

The contents of the book are now outlined.

sets the goals of the book.

.

Propositional logic is studied in . This includes the syntax and semantics of propositional logic. Gentzen systems are introduced as a method for attempting to falsify a proposition. The completeness theorem is shown as well as some of its consequences (the conjunctive and disjunctive normal forms).By introducing infinite sequents, the extended completeness theorem and the compactness theorem are obtained. An infor-mal exposition of the complexity classes P, NP, and of the concept of NP-completeness is given at the end of the Chapter.