Saarland University Computer Science

Introduction to Computational Logic Prof. Gert Smolka, Tobias Tebbi


Lecture Notes

Coq Files

Please use Base.v for your Coq developments. To do so, put it in the same directory and compile it by entering "coqc Base.v" in the command line.

Afterwards, add "Require Import Base." to your source file. 




  • 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