See the mailing list archives for announcements and updates.

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

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:

- The obvious application is computer-assisted mathematics: automated reasoning systems have, on occasion, solved open mathematical problems.
- The software and hardware verification problems (i.e.: how one can be sure that a program or digital device performs according to specification) are often stated as problems in logic. In contrast to mathematical problems, which are interesting and unique, verfication problems are copious, similar to each other and very dull - exactly the kind of material that computers handle well and humans badly. Verification is thus an important application area for automated reasoning techniques and systems, and it is here where they probably can do most good.
- Some advanced database systems use automated reasoning techniques.

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

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:

- well-formed formulae and well-formed terms
- free and bound variables
- semantics of first-order logic (models and interpretations) -- recommended
- inference rule and inference in first-order logic

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 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]

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.

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.

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:

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

- Chapter 1: Introduction
- Chapter 2: A Precis on Logic
- Chapter 3: The ground case
- Chapter 4: First-order generalizations
- (Final lecture presentation: A Peek Beyond the Basics)

**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>