Site Map | College of Engineering | UC Davis | MyUCDavis

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%)

Catalog Description:
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:

  1. Overview of Known Techniques
    1. The limitations of automated deduction
    2. Complete versus incomplete methods
  2. Resolution Methods
  3. Term Rewriting
    1. Equational logic
    2. Confluence
    3. Normal form
    4. Proof methods
  4. Methods of improving efficiency. Set of support, relevance, forward and backward chaining, abstraction and generalization
  5. Automation of Induction
    1. Computation induction
    2. Structural induction
  6. Decision Procedures. Special Theories.
  7. 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.

Textbooks:
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

Back to Course Descriptions