Saarland University Computer Science

Introduction to Computational Logic Prof. Gert Smolka, Dr. Chad Brown


Lecture Notes

Coq Files




  • 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)
  • The Univalent Foundations Program
    Homotopy Type Theory.
    Institute for Advanced Study, Princeton, 2013.
  • 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.
  • Henk Barendregt, Wil Dekkers, Richard Statman,
    Lambda Calculus with Types.
    Cambridge University Press, 2013.
  • Biographies of important logicians