Logic for Computer Science:
Foundations of Automatic Theorem Proving

Jean Gallier
Wiley, pp. 511 (1986).

Out of print.

The copyright has now reverted to me. See below for a corrected and revised on-line version.

---

REVISED ON-LINE VERSION (2003)

YOU CAN NOW DOWNLOAD THE ENTIRE BOOK !!

Terms and Conditions

• 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.  

Note that because the original Tex file contains certain macros producing Postcript, I was unable to produce pdf output of certain pages directly. Those pages were converted from ps files to pdf files.

• Entire book, compressed file (ps.gz)   (pdf.gz)

• Preface, Table of Contents (ps)   (pdf)
• Chapters 1, 2 (ps)   (pdf)
• Chapter 3 (ps)   (pdf)
• Chapter 4 (ps)   (pdf)
• Chapter 5 (ps)   (pdf)
• Chapter 6 (ps)   (pdf)
• Chapter 7 (ps)   (pdf)
• Chapter 8 (ps)   (pdf)
• Chapter 9 (ps)   (pdf)
• Chapter 10 (ps)   (pdf)
• Appendix (ps)   (pdf)
• References, Index, Tables (ps)   (pdf)

---

ERRATA TO 1985 EDITION

• Typos and errors (1985 Edition) (ps)   (pdf)

---

OTHER LOGIC PAPERS OF INTEREST

• Snyder, W. and Gallier, J. Higher-Order Unification Revisited: Complete Sets of Transformations.
  Journal of Symbolic Computation, 8(5), 101--140 (1989).
  (ps)   (pdf)

• Snyder, W. and Gallier, J. Complete Sets of Transformations for General E-Unification.
  Theoretical Computer Science, 67, 203-260 (1989).
  Part I (ps),   (pdf),   Part II (ps),   (pdf)

• Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi.
  Theoretical Computer Science, 110(2), 249-239 (1993).
  (ps)   (pdf)
  

• Constructive Logics. Part II: Linear Logic and Proof Nets.
  Technical Report, CIS Department, University of Pennsylvania, 1991.
  (ps)   (pdf)

• On the Correspondence Between Proofs and lambda-Terms.
  Cahiers du Centre de Logique, Philippe DeGroote, Editor, Université Catholique de Louvain, 1995.
  (ps)   (pdf)

• On Girard's "Candidats de Reductibilite'." In Logic and Computer Science, Odifreddi, editor, Academic Press, 123-203 (1990).
  Part I (ps),   (pdf),   Part II (ps),   (pdf)   Part III (ps),   (pdf),   Part IV (ps),   (pdf)

• Proving Properties of Typed lambda-Terms Using Realizability, Covers, and Sheaves.
  Theoretical Computer Science, 142(2), 299-368, (1995).
  (ps)   (pdf)

• Kripke Models and the (in)equational logic of the second-order lambda-Calculus
  Annals of Pure and Applied Logic , 84, 257-316, (1997)
  (ps)   (pdf)

• Typing untyped lambda terms, or Reducibility Strikes Again!
  Annals of Pure and Applied Logic , 91, 231-270, (1998)
  (ps)   (pdf)

• A proof of strong normalization for the theory of constructions using a Kripke-like interpretation.
  (With Thierry Coquand) First Annual Workshop on Logical Frameworks, Antibes, May 1990.
  (ps)   (pdf)

• A Note on Logical PERs and Reducibility. Logical Relations strike again!
  Technical Report, December 1998.
  (ps)   (pdf)

• Unification Procedures in Automated Deduction Methods Based on Matings: A Survey.
  In Tree automata and languages, Edited by M. Nivat and A. Podelski, Elsevier, 439-485 (1992).
  (ps)   (pdf)

• The completeness of propositional resolution, A simple constructive proof (July, 2005).
  (ps)   (pdf)

 

Back to Gallier's books (complete list)

Back to Gallier Homepage

---

Jean Gallier
2003-6-6