1997 Fall Quarter
Lecture: 3 hours
Techniques of mechanical theorem proving. Methods based on resolution and termrewriting. Decision procedures. Induction. Applications to program verification, question/answering and plan generation. Study existing mechanical theorem provers.
PHI 112; or MAT 125 or familiarity with first order logic.