Foundations of Automatic Theorem Proving

A corrected version of the original Wiley edition (pp. 511, 1986) is going to be published by Dover in 2014.

REVISED DOVER EDITION (2014)

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

- Preface, Table of Contents, Introduction (pdf)

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

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