CS
408: Automated Reasoning
Course Syllabus  Spring 1998
Professor: C. Lynch
Office: 371 Science Center
Phone: 2682384
Email: clynch@sun.mcs.clarkson.edu
Office Hours: M,W 9:0010:00 and 1112:00; F 9:0010: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, realtime
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
clynch@sun.mcs.clarkson.edu
