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, firstname.lastname@example.org.
Office Hours. M 3-4, W 2-4, F 2-4
Reading. Here is the reading material
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: