Saarland University
Informatics
Programming Systems
Teaching
ICL 2006


Main page
Timetable
Literature
Lecture notes
Registration
Services
Exams and Grade
Login
Mailing list

Introduction to Computational Logic: Lecture Notes

1. Formulas as terms
2. Axiomatization of terms
3. Structures and Specifications
4. Equational Deduction
   • Slides 2006/6/12 Parameters
   • Slides 2006/6/14 Closed Specifications and Conversion Proofs
   • Slides 2006/6/19+21 Entailment relations, inference systems, and confluent relations
5. Boolean Algebra
   • Slides 2006/6/7 Prime Trees
   • Slides 2006/6/12 BDDs
   • Slides 2006/6/14 Clause Forms
6. Propositional Logic
   • Slides 2006/6/26+28
7. Predicate Logic
   • Slides 2006/7/3+5 (Quantifiers)
   • Slides 2006/7/10 (Choice)
   • Slides 2006/7/12 (Identity)
   • Slides 2006/7/17+19 (First-Order Completeness)

Lecture notes from previous runs of this course: Summer 2005, Summer 2004.

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

The course assume familarity with basic functional programming in the programming language Standard ML. Some useful links:

• Programming in Standard ML, by Robert Harper, CMU.
• Programmierung, by Gert Smolka. An introduction to programming using Standard ML (in German).
• Moscow ML. A nice implementation of Standard ML.
• Alice. Another implementation of Standard ML with a nice GUI.
• The Standard ML Basis Library
• Comp.Lang.ML FAQ