CS 408: Automated Reasoning
Course Syllabus -- Spring 1998

Professor: C. Lynch
Office: 371 Science Center
Phone: 268-2384
E-mail: clynch@sun.mcs.clarkson.edu

Office Hours: M,W 9:00-10:00 and 11-12:00; F 9:00-10:00 a.m. and by appointment

Text: Automated Reasoning: Introduction and Applications by Wos, Overbeek, Lusk, and Boyle (McGraw Hill, 1992).

Course Objectives: This course will study the foundations and applications of programs which are used to deduce information and prove theorems. Assignments will be to program a simple automated reasoning program, use a powerful existing program, and examine completeness and efficiency issues. Topics include representation of knowledge, inference rules, and search strategies. Applications are from the fields of abstract mathematics, formal logic, logic circuit design and validation, real-time system control, program verification, and the design of logic programming languages.

Software: You will need a copy of the theorem prover OTTER. You can download it from http://www.mcs.anl.gov/home/mccune/ar/otter/index.html

Exams: Tentative dates for Exam 1 and 2 are: 3/4, 4/8.

Grading Policy:

Exam 1 25%
Exam 2 25%
Homeworks 30%
Project 20%

Contents: I will cover chapters 1 through 6 and chapters 15 and 16 in the book. These chapters wil introduce some puzzles which give an idea of what an automated reasoning program is useful for. It also will give some formal definitions necessary to understand the syntax and semantics of the language. I will supplement this material with current information about efficient theorem provers. Particularly, I will discuss the topic of equality. Chapters 7 through 14 address different applications of automated reasoning programs. We will cover as much of this material as we can.

Homeworks will include pencil and paper assignments to test your understanding of the basic material, programming assignments where you need to build parts of an automated reasoning application, and assignments where you will use OTTER to prove theorems. The homeworks will be individual assigments, not team projects. The homeworks will have due dates. I will follow a strict policy of taking off five points per day for the first week of each late homework assignment, and ten points a day for the second week.

When we discuss the different applications of automated reasoning programs in chapters 7 throught 14, students will make presentations. The projects will be based on the material in those presentations.

Since this is my active area of research, I am preparted to discuss any topic in this field. Since this is a small class, we can take the students interests in mind when we decide what topics to cover.

Last modified: 20 January 1998