Logic for Computer Science:
Foundations of Automatic Theorem Proving
Second Edition

Jean Gallier

A corrected version of the original Wiley edition (pp. 511, 1986), published by Dover, June 2015.

---

DOVER EDITION (June 2015)

Terms and Conditions

• By downloading these files you are agreeing to the following conditions of use: Copyright 2015 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.  

• Preface, Table of Contents   (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)

• On Girard's "Candidats de Reductibilite'."
  In Logic and Computer Science. P. Odifreddi, Editor, Academic Press, 123-203 (1989).
  (pdf)  

• What's so special about Kruskal's Theorem and the ordinal Gamma_0.
  A survey of some results in proof theory.
  Annals of Pure and Applied Logic, 53, 199-260 (1991).
  (pdf)

• Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi.
  Theoretical Computer Science, 110(2), 249-339 (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)

• 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.
  LMCS, 2(5), pp. 1-7, (November, 2006).
  (html)   (pdf)

 

Back to Gallier's books (complete list)

Back to Gallier Homepage

---

Jean Gallier
2003-6-6