Logic for Computer Science: Foundations of Automatic Theorem Proving by Jean Gallier is available in ps and pdf formats. 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 (Chapters 6,7,9,10) 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.
Table of Contents
- Mathematical Preliminaries
- Propositional Logic
- Resolution In Propositional Logic
- First-Order Logic
- Gentzen’s Cut Elimination Theorem And Applications
- Gentzen’s Sharpened Hauptsatz; Herbrand’s Theorem
- Resolution In First-Order Logic
- Sld-Resolution And Logic Programming (Prolog)
- Many-Sorted First-Order Logic
Format(s): PDF, PostScript
File size: 6.99 MB
Number of pages: 534