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 203 or 303 and CS 202 or 302, or consent of instructor.
Note Open to graduate students. Graduate students are required to do additional work of a research nature.