ECS 274 AUTOMATED DEDUCTION (4) III
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:
- Overview of Known Techniques
- The limitations of automated deduction
- Complete versus incomplete methods
- Resolution Methods
- Term Rewriting
- Equational logic
- Normal form
- Proof methods
- Methods of improving efficiency. Set of support, relevance, forward and backward chaining, abstraction and generalization
- Automation of Induction
- Computation induction
- Structural induction
- Decision Procedures. Special Theories.
- Hands-on experience with several contemporary theorem provers, e.g., HOL, PVS, NQTHM — which will familiarize the students with how the different theorem proving paradigms are mechanized in practice.
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