Description Elements of formal logic; various approaches to automation including resolution; restrictions and search methods; inductive theorem-proving; Knuth-Bendix completion; Boyer-Moore theorem-prover; applications.
Prerequisites A grade of C or better in both CS 202 and CS 303, or consent of instructor.
Note Open to graduate students. Graduate students are required to do additional work of a research nature.