Introduction to Computational Logic: Resources
Lecture Notes
Coq
Literature
-
Zhaohui Luo,
Computation and Reasoning: A Type Theory for Computer Science.
Oxford University Press, 1994.
-
Henk Barendregt and Herman Geuvers,
Proof-checking using Dependent Type Systems.
Handbook of Automated Reasoning, Volume II, 1149--1240.
Elsevier 2001.
-
Jean-Yves Girard,
Proofs and Types.
Cambridge University Press, 1990.
-
Dag Prawitz,
Natural Deduction, a Proof-theoretical Study.
Dover Publications, 2006. (first published 1965)
-
Yves Bertot and Pierre Castéran,
Interactive Theorem Proving and Program Development.
Coq'Art: The Calculus of Inductive Constructions.
Springer, 2004.
-
Thomas Forster,
Logic, Induction and Sets.
Cambridge University Press, 2003.
-
Melvin Fitting,
First-Order Logic and Automated Theorem Proving. 2nd edition.
Springer, 1996.
-
Herbert B. Enderton,
A Mathematical Introduction to Logic. 2nd edition.
Academic Press, 2001.
-
Peter B. Andrews,
An Introduction to Mathematical Logic and Type Theory:
To Truth Through Proof.
Kluwer Academic Publishers, 2002.
-
Patrick Blackburn, Maarten de Rijke and Yde Venema,
Modal Logic.
Cambridge University Press, 2001.
-
J. Roger Hindley and Jonathan P. Seldin,
Lambda Calculus and Combinators: An Introduction.
Cambridge University Press, 2008.
-
Anne S. Troelstra and Helmut Schwichtenberg,
Basic Proof Theory. 2nd edition.
Cambridge University Press, 2000.
-
Franz Baader and Tobias Nipkow,
Term Rewriting and All That.
Cambridge University Press, 1998.
-
Biographies of important logicians
Last Change: Thu 01 Jan 1970 00:00:00 UTC
