CS 653 Automated Reasoning
Spring 2009


Official Course Description. This course will cover advanced topics in Automated Reasoning research. Students will gain experience reading and discussing research papers. Students will be expected to conduct research-related work in Automated Reasoning.

Prerequisites. CS541 and CS547 or consent of the instructor

Location and Times. Science Center 303, TTh 2:30-3:45

Instructor. Chris Lynch. Science Center 377, 268-2384, clynch@clarkson.edu.

Office Hours. M 3-4, W 2-4, F 2-4

Required Text.

Reading. Here is the reading material

Course Objectives.

  1. To learn the basic concepts and results of Automated Reasoning.

  2. To become familiar with some of the current research topics in Automated Reasoning.

  3. To gain experience reading research papers in computer science.
Demonstrable outcomes. By the end of the semester,
  1. You will be familiar with and understand basic results and research-related topics in Automated Reasoning.

  2. You will be able to solve problems related to this material.

  3. You will be able to read and understand research papers in Automated Reasoning.

Tentative list of topics. Decision Procedures, Combination of Decision Procedures, Satisfiability, Satisfiability modulo theories, Theorem proving in first order logic, Unification, Unification modulo theories, Term Rewriting, Interactive and Higher Order Theorem Proving.

Grading. Throughout this semester, we will read several research papers on Automated Reasoning. We will discuss the research papers in class. Part of your grade will be based on your participation in these discussions, your presentation of some of the material, and homeworks I will assign on this material. You will also be expected to do a research project, which will form the other part of your grade. Your course grade will be computed using the following formula:

50% Participation and Presentation and Homework + 50% Project