Subjects include automated reasoning techniques for propositional logic, first-order logic, linear arithmetic over reals and integers, theory of uninterpreted functions, and combinations of these theories. Examines automated logical reasoning both from a theoretical and practical perspective, giving a hands-on experience building useful tools, such as SAT and SMT solvers. Three lecture hours a week for one semester. Only one of the following may be counted: Computer Science 389L, 395T (Topic: Automated Logical Reasoning), Artificial Intelligence 389L. Prerequisite: Graduate standing.