Introduction to Computational Logic Prof. Gert Smolka, Tobias Tebbi

Lecture Notes

• Lecture notes (from 2014)
• Better presentation of proof of generalized cut lemma 2.2.1

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. 

• ICL Base library (Base.v)
• Propositional Entailment (PropL.v)
• Classical tableaux (ctab.v)
• Gentzen System (Gentzen.v)
• Beautified proof of cut lemma genC'

Videos

Coq

• Coq Home Page (download system here, we are using version 8.4)
• There are two user interfaces for Coq: CoqIDE and Proof General. You can choose which one you want to use.
  • CoqIDE: You can download and install CoqIDE along with the rest of Coq from the Coq Home Page. Documentation about CoqIDE can be found here.
  • Proof General: Proof General is an emacs mode that supports many theorem provers, including Coq. You can download Proof General from this link.
• Coq Documentation
• An online book on software foundations starting with an introduction to Coq 
  (by Benjamin Pierce and others)
• A book on certified programming with dependent types using Coq 
  (by Adam Chlipala)

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