Explore automated reasoning techniques for propositional logic, first-order logic, linear arithmetic over reals and integers, theory of uninterpreted functions, and combinations of these theories. Examine automated logical reasoning both from a theoretical and practical perspective, including 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.