Saarland University
Computer Science
Programming Systems
Teaching
ICL 2005


Main page
Timetable
Literature
Lecture notes
Registration
Services
Exams
Review your data
Mailing list

Introduction to Computational Logic: Lecture Notes

The course assumes familarity with basic functional programming and Standard ML as it is taught in our beginners course Programmierung 1. We recommend Moscow ML or Alice as Standard ML interpreter. Alice has a nice programming environment well-suited for novices.

There are lecture notes Gert Smolka has written for previous runs of this course. They are in German. The most recent version is from Summer 2004. Although we will present things somewhat differently this year, the notes from 2004 are highly recommended.

Biographies of important logicians are available at www-history.mcs.st-andrews.ac.uk.

1. Simply Typed Lambda Calculus and Equational Deduction (weeks 1-3+10)
   • Implementation of S in Standard ML (April 18+20)
   • Equational Deduction (April 25+27)
   • Conservative Entailment (May 2)
   • Closure Operators and Entailment Relations (June 13)
   • Equational Reasoning (June 15)


2. Propositional Logic (weeks 4-8)
   • Boolean Equations (May 2+4)
   • Decision Trees and Tautology Theorem (May 9+11)
   • Clause Forms (May 18)
   • Sequent Calculus (May 23)
   • Natural Deduction (May 25+30)
   • Higher-order Boolean Logic (June 1)
   • Proof of f(f(f x))= f x (June 25)
   
   
   • Extra: Gert Smolka: Slides of a Talk on Solving Boolean Equations (2003)
   • Extra: Gerhard Gentzen: Untersuchungen über das logische Schließen(April 2004)
   • Extra: Frank Pfenning: Lecture Notes on Automated Theorem Proving (April 2004)


3. Quantifiers and Identity (weeks 9-11)
   • Quantifiers (June 8)
   • Formula Convention and Linear Proofs (June 15)
   • Identities (June 20)
   • Review of S(HOL) (June 22)
   • Choice Operator (June 25)
   • Quick Reference Guide to S(HOL) (June 26+29)
   
   
   • Extra: Gert Smolka: Slides of a Talk on S(HOL) (June 2005)
   • Extra: Mark Kaminiski's Bachelor's Thesis on S(HOL) (May 2005)
   
   
4. Dynamic Logic and Computability (weeks 12-14)
   • Regular Programs (June 30)
   • Program Verification (July 6)
   • Computability (July 15)
   
   
   • Extra: Dexter Kozen: Kleene algebra with tests (1997)