Lecture: 3 hours
Discussion 1 hour
Prerequisite: Math 125 or Philosophy 112 or familiarity with first-order logic
Grading: Letter; homework (25%), midterm (25%), final (25%), project (25%)
Techniques of mechanical theorem-proving. Methods based on resolution and term-rewriting. Decision procedures. Induction. Applications to program verification, question/answering and plan generation. Offered in alternate years.
Expanded Course Description:
Selected from the current literature.
Engineering Design Statement:
Using a contemporary theorem power, verify a small but realistic design with respect to requirements for the design. Designs of interest would include communication protocols, clock synchronization, a composable system, voting protocols.
ABET Category Content:
Engineering Science: 3 units
Engineering Design: 1 unit
Instructor: K. Levitt
Prepared by: K. Levitt (February 1997)
THIS COURSE DOES NOT DUPLICATE ANY EXISTING COURSE
Last revised: 2/97