TIE 329 Automated Reasoning, spring 2004

Korppi page

See the mailing list archives for announcements and updates.

Syllabus

This course is worth 2 credits (4 in the ECTS system). It is lectured in English.

Overview

The aim of this course is to introduce you to the basic techniques used in automated reasoning, including resolution and semantic tableaux, and to show how logical information can be processed by programs. The course is partly theoretical and partly practical. We will in the end have constructed a computer program that can solve simple logical problems.

Automated reasoning is about mechanising logic. Its roots are deep in artificial intelligence, but it has since emerged as an independent field of study, in fact one of the most challenging ones in computer science. The dream of a reasoning machine is centuries old, but when mathematicians discovered cracks in the foundation of their discipline and tried to patch it by investigating logic, they made a discovery that appeared to destroy the field of automated reasoning even before it was born: they proved that there is no general algorithm that can decide on the truth of a first-order proposition. Even the simpler problems have only prohibitively expensive algorithms (from NP-complete to super-exponential complexity). However, it was not an end: it was the beginning.

There is an old joke about a shop that promises immediate delivery for all orders, except for impossible ones, for which the delivery may take up to two weeks. In similar spirit, these discoveries have only slowed down the search for the reasoning machine. While no algorithms exist, the same does not hold for semi-algorithms: a machine can confirm truths, while it may fail to produce an answer when presented a falsehood. As to the problem of combinatorial explosion, the major part of automated reasoning research is coming up with mechanisms that can tell the relevant from the irrelevant (and there lies the challenge).

Automated reasoning has applications:

For a perspective on automated reasoning, read Tim Andrew Obermiller's biography of Larry Wos.

Prerequisities

We will build heavily on first-order logic (a.k.a. predicate logic); you must be familiar with it. We will spend some time at the beginning rewieving first-order logic, but it will all fly over your head if you have had no previous exposure to it. Therefore, you should be familiar with the following terms and concepts:

This material is covered by the University's two mostly interchangable courses on logic, MAT 223 and FIL A31. Any introductory book on modern logic or mathematical logic will also cover them. Rantala & Virtanen: Logiikan peruskurssi is an online text on logic that should be sufficient (only in Finnish, though).

Many examples are drawn from mathematics and set theory, so familiarity with them is a bonus. Mathematical experience (gained by studying mathematics, regardless of the topic) will be extremely useful.

Basic hands-on knowledge on regular expressions, context-free grammars and parsing is required. Try writing a simple unambiguous context-free grammar for arithmetic expressions; if you have problems, you should brush up your skills. A passing familiarity with computability theory (Turing machines, halting problem, undecidability) is also necessary. These topics are covered by the Automata and formal languages course (TIE 264). Grammars, regular expressions and parsing is covered by books on compiler construction, as well as by books on automata theory. Computability theory is covered by books on that subject.

Algorithms and example programs will be given in a functional style, using the Haskell programming language. While knowledge of Haskell and the functional style are useful, they are not necessary. Features of the language will be explained when they are needed, and the more tricky (or "hackerish") idioms will be avoided. For programming exercises, any programming language can be used.

Lectures

Lectures are held Tuesdays at 14-16 and Fridays at 10-12 on weeks 10-15 (first lecture is on 2004-03-02 and the last is on 2004-04-06). All lectures are held in Agora Beeta (first floor). Lecture attendance is voluntary but highly recommended.

All lecture attendants are encouraged to keep a learning journal A well-made lecture log will partially or completely supplant the exam. [details]

The lecturer-examiner

I am Antti-Juhani Kaijanaho. I am the lecturer and examiner in this course. You can reach me by email at <antkaij@mit.jyu.fi>, by phone at (014) 260 2766 (the central will take a message if I am absent - let it ring) and by foot at AgC 416.1. I try my best to be available during my office hours (every Wednesday between 12 and 14); at other times, making an appointment is recommended. I will also be available for a few minutes after every lecture.

Exercises

Each week, a set of take-home exercises will be given. They are then discussed on the next week's exercise session. The first exercise session will be held on week 11 (2004-03-08/14). Each session is on Wednesdays at 14-16 in Ag Alfa. Exercises contribute to the overall score used in grading.

Group work in exercises is permitted and encouraged, so long as everybody who has participated in creating an answer is given credit.

Exams and grading

Grades will be assigned based on an exam. Exam dates can be found from Korppi.

A lecture log, depending on its quality, and exercise activity will supplant parts or all of the exam.

Past exams:

Readings

There is no textbook. A companion booklet is distributed piecemeal in the lectures and here (in PDF):

Do not print the booklet on University printers! Rather, come and get a copy from me.

As optional supplemental reading I recommend especially Melvin Fitting's First-Order Logic and Automated Theorem Proving (second edition, Springer, 1996). This book is a graduate (post-baccalaureate) textbook on first-order logic and automated reasoning. It presents most of the material we will cover in this course, and it can also be used to fill any gaps you may have in your logical training.

Another suggested optional supplemental reading is Wos and others' Automated reasoning - introduction and applications (Prentice-Hall, 1984), a rather old but quite readable account on automated reasoning issues and techniques.

To anyone who is serious about getting into the field of automated reasoning, Robinson and Voronkov's (eds) Handbook of automated reasoning (North-Holland [Elsevier] and MIT Press, 2001) is an indispensable reference. Its price makes it unaffordable to anyone else, though.

Loveland's Automated theorem proving: a logical basis (North-Holland, 1978) is an old theoretical account on the state of the art in the end of the 1970's.


2004-04-19 <antkaij@mit.jyu.fi>