First-Order Logic and Automated Theorem Proving

by Melvin Fitting

There are many kinds of books on formal logic. Some have philosophers as their intended audience, some mathematicians, some computer scien­ tists. Although there is a common core to all such books, they will be very different in emphasis, methods, and even appearance. This book is intended for computer scientists. But even this is not precise. Within computer science formal logic turns up in a number of areas, from pro­ gram verification to logic programming to artificial intelligence. This book is intended for computer scientists interested in automated theo­ rem proving in classical logic. To be more precise yet, it is essentially a theoretical treatment, not a how-to book, although how-to issues are not neglected. This does not mean, of course, that the book will be of no interest to philosophers or mathematicians. It does contain a thorough presentation of formal logic and many proof techniques, and as such it contains all the material one would expect to find in a course in formal logic covering completeness but, not incompleteness issues. The first item to be addressed is, What are we talking about and why are we interested in it? We are primarily talking about truth as used in mathematical discourse, and our interest in it is, or should be, self­ evident. Truth is a semantic concept, so we begin with models and their properties. These are used to define our subject.

Genres: Logic, Philosophy

326 pages, Kindle Edition

First published April 28, 1990

About the author

Melvin "Mel" Fitting (born January 24, 1942) is a logician with special interests in philosophical logic and tableau proof systems. He was a Professor at City University of New York, Lehman College and the Graduate Center from 1968 to 2013. At the Graduate Center he was in the departments of Computer Science, Philosophy, and Mathematics, and at Lehman College he was in the department of Mathematics and Computer Science. He is now Professor emeritus.

Fitting was born in Troy, New York. His undergraduate degree is from Rensselaer Polytechnic Institute, and his doctorate is from Yeshiva University, both in mathematics. His thesis advisor was Raymond Smullyan.

In June 2012 Melvin Fitting was given the Herbrand Award by CADE, for distinguished contributions to automated deduction.

A loose motivation for much of Melvin Fitting's work can be formulated succinctly as follows. There are many logics. Our principles of reasoning vary with context and subject matter. Multiplicity is one of the glories of modern formal logic. The common thread tying logics together is a concern for what can be said (syntax), what that means (semantics), and relationships between the two. A philosophical position that can be embodied in a formal logic has been shown to be coherent, not correct. Logic is a tool, not a master, but it is an enjoyable tool to use