CSE 545T: Introduction to Automated Theorem Proving, Fall 2007

location:	Lopata Hall, Room 229
times:	1:00PM-2:30PM, Tuesdays and Thursdays

Topic. This class is about performing logical deductions on a computer. There are two basics parts to the topic (and this course): algorithms that can automatically perform enough deductions to prove formulas or test validity of formulas; and formalisms and software tools which help a human prove theorems more-or-less by hand. We will learn the Isabelle proof assistant as an example of the latter. The goal of the course is to introduce automated theorem proving from a practical point of view: the emphasis will be on using existing tools and implementing existing algorithms, rather than on the theoretical techniques needed to design new algorithms.

Prerequisites. To take this class, you should be familiar with the basic syntax and semantics of propositional (ANDs, ORs, and NOTs) logic and first-order (FORALL, THERE EXISTS) logic. Also, you should have some programming experience, because the work for the course includes a programming project. More sophisticated background than that is not assumed.

Work. The graded work for the course consists in two projects, each worth 50% of the semester grade. The projects cover the two basic parts of the class mentioned above.

Lab. Throughout the semester, we will occasionally have class in the CEC linux laboratory.

Staff. The professor is Aaron Stump, office Bryan 523, office phone 314-935-4465. Office hours are by appointment or right after class.