Lecture, four hours; discussion, two hours; outside study, six hours. Requisite: course 161. Introduction to theory and practice of automated reasoning using propositional and first-order logic. Topics include syntax and semantics of formal logic; algorithms for logical reasoning, including satisfiability and entailment; syntactic and semantic restrictions on knowledge bases; effect of these restrictions on expressiveness, compactness, and computational tractability; applications of automated reasoning to diagnosis, planning, design, formal verification, and reliability analysis. Letter grading.