CSCI 643 - Automated Logical Reasoning

Fall or Spring 3 Prerequisite(s): Knowledge of algorithms and finite automata.

Automated logical reasoning has enabled substantial progress in many fields of computer science, including software and hardware verification, theorem proving, program analysis, and artificial intelligence. In this course, we will study widely-used logical theories and decision procedures for answering whether formulas in these theories are satisfiable. In particular, we will consider automated reasoning techniques for propositional logic, firstorder logic, linear arithmetic over reals and integers, theory of uninterpreted functions, and combinations of these theories. This course will examine automated logical reasoning both from a theoretical and practical perspective, giving interested students a hands-on experience building useful tools, such as SAT solvers.