22c:245 - Advanced Artificial Intelligence

Spring 2002

Course Syllabus

Instructor

Cesare Tinelli
201E MLH
335-0735
tinelli@cs.uiowa.edu

Office hours: Mon 3:30-5pm, Wed 2-3:30pm, or by appointment.

Lectures

TuTh 2:30-3:45pm, 113 MacLean Hall.

Prerequisites

22C:145 and/or consent of instructor. Familiarity with propositional or first-order logic is required.

Web Page

Most of the information about the class, including handouts and reading assignments, will be available from the class web site: http://goedel.cs.uiowa.edu/245/

Course Description

This course is an introduction to Automated Reasoning, the field of Computer Science concerned with the discovery, design and implementation of methods to mechanize deductive logical reasoning. These methods have been applied successfully to solve difficult problems in a variety of areas, including verification (of hardware, software, cryptographic protocols, message-passing systems), planning, program generation, and pure mathematics.

The course begins with the syntax and semantics of first-order logic, and basic concepts such as inference system, proof, soundness and completeness, up to the Herbrand theorem, the key compactness result that makes automated deduction in first-order logic possible. Then it proceeds with an illustration of some of the major classes of methods for automated deductive reasoning, namely instance-based methods (e.g. the Davis-Putnam procedure), subgoal-reduction methods (e.g., tableaux), and saturation-based methods (e.g., resolution) and their refinements. The presentation emphasizes the control issues and the search techniques that make these strategies work in practice.

Course Objectives

The main objective of this course is to expose the students to the main principles and techniques of automated reasoning. At the same time the course is designed to contribute to the students' professional growth as computer scientists by

developing their ability to read research papers critically, by recognizing main points and contributions, and identifying strengths and weaknesses;
developing their ability to devise and run experiments, and analyze their results;
refining their communication skills; in particular, the ability to present research work to an audience, and to discuss technical material with peers.

Assignments and Exams

There will be written assignments and machine problems. Normally, the assignments will consist in providing mathematical proofs. Machine problems will involve the use of an automated reasoning tool.
There will be no exams in this course.

Projects

There will be two mini-projects, having one of the following formats.

Readings project:
with the assistance of the instructor the student chooses one or two related articles in the literature, studies them, and presents them in class.
Experimental project:
with the assistance of the instructor the student chooses a small set of related automated reasoning problems, runs them on a publicly available automated reasoning system (downloaded and installed by the student), and presents the experiments and their results in class.

Each presentation will be reviewed by the rest of the class.
Students can choose their projects based on their interest and the material covered in class. All projects are individual and must be different.

Textbook and Readings

The adopted textbook is

Deduction Systems by Rolf Socher-Ambrosius and Patricia Johann,
Graduate Texts in Computer Science, Springer, 1996.

A list of additional reading material will be available on the course webpage.

Grading

The weighting of items in grade determination will be approximately the following: homework assignments 40%, participation to class discussion 10%, mini-projects 25% each.

Computing Facilities

We will use the HP and Linux workstations in the CS Educational Lab in 301 MLH. Please see the instructor after class if do not have a CS account yet.

Special Needs

The instructor must hear from anyone who has a disability that may require some modification of seating, testing, or other class requirements so that appropriate arrangements can be made. Please see the instructor after class or during office hours.