Logic for Computer Science:
Foundations of Automatic Theorem Proving
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
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
ERRATA TO 1985 EDITION
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).
- Snyder, W. and Gallier, J.
Complete Sets of Transformations for General E-Unification.
Theoretical Computer Science, 67, 203-260 (1989).
Part I (ps),
Part II (ps),
- On Girard's "Candidats de Reductibilite'."
In Logic and Computer Science. P. Odifreddi, Editor, Academic Press, 123-203 (1989).
- 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,
- Constructive Logics. Part I: A Tutorial on Proof Systems and Typed
Theoretical Computer Science, 110(2),
- Constructive Logics. Part II: Linear Logic and Proof Nets.
Technical Report, CIS Department, University of Pennsylvania, 1991.
- On the Correspondence Between Proofs and lambda-Terms.
Cahiers du Centre de Logique, Philippe DeGroote, Editor,
Catholique de Louvain, 1995.
- Proving Properties of Typed lambda-Terms Using Realizability,
Covers, and Sheaves.
Theoretical Computer Science, 142(2),
- Kripke Models and the (in)equational logic of the second-order
Annals of Pure and Applied Logic , 84,
- Typing untyped lambda terms, or Reducibility Strikes Again!
Annals of Pure and Applied Logic , 91, 231-270, (1998)
- 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.
- A Note on Logical PERs and Reducibility.
Logical Relations strike again!
Technical Report, December 1998.
- Unification Procedures in Automated Deduction Methods Based on Matings:
In Tree automata and languages,
Edited by M. Nivat and A. Podelski, Elsevier, 439-485 (1992).
- The completeness of propositional resolution, A simple
LMCS, 2(5), pp. 1-7, (November, 2006).
Gallier's books (complete list)