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**: 18,412

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.

Terms and Conditions:

Book Excerpts:

Review(s):

Jean Gallier wrote:By downloading these files you are agreeing to the following conditions of use: Copyright 2003 by Jean Gallier. This material may be reproduced for any educational purpose, multiple copies may be made for classes, etc. Charges, if any, for reproduced copies must be no more than enough to recover reasonable costs of reproduction. Reproduction for commercial purposes is prohibited. The cover page, which contains these terms and conditions, must be included in all distributed copies. It is not permitted to post this book for downloading in any other web location, though links to this page may be freely given.

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):

Tweet

About The Author(s)

Jean H. Gallier is a professor at Computer and Information Science Department, School of Engineering and Applied Science, University of Pennsylvania. His research interests include geometry and its applications (3D graphics, computer vision), geometric modeling, geometry of curves and surfaces, algebraic geometry, differential geometry, and medical imaging.

Book Categories

Computer Science
Introduction to Computer Science
Introduction to Computer Programming
Algorithms and Data Structures
Artificial Intelligence
Computer Vision
Machine Learning
Neural Networks
Game Development and Multimedia
Data Communication and Networks
Coding Theory
Computer Security
Information Security
Cryptography
Information Theory
Computer Organization and Architecture
Operating Systems
Image Processing
Parallel Computing
Concurrent Programming
Relational Database
Document-oriented Database
Data Mining
Big Data
Data Science
Digital Libraries
Compiler Design and Construction
Functional Programming
Logic Programming
Object Oriented Programming
Formal Methods
Software Engineering
Agile Software Development
Information Systems
Geographic Information System (GIS)

Mathematics
Mathematics
Algebra
Abstract Algebra
Linear Algebra
Number Theory
Numerical Methods
Precalculus
Calculus
Differential Equations
Category Theory
Proofs
Discrete Mathematics
Theory of Computation
Graph Theory
Real Analysis
Complex Analysis
Probability
Statistics
Game Theory
Queueing Theory
Operations Research
Computer Aided Mathematics

Supporting Fields
Web Design and Development
Mobile App Design and Development
System Administration
Cloud Computing
Electric Circuits
Embedded System
Signal Processing
Integration and Automation
Network Science
Project Management

Operating System
Programming/Scripting
Ada
Assembly
C / C++
Common Lisp
Forth
Java
JavaScript
Lua
Microsoft .NET
Rexx
Perl
PHP
Python
R
Rebol
Ruby
Scheme
Tcl/Tk

Miscellaneous
Sponsors