Computer Science 345 - Automated Reasoning

This course will explore the theory and practice of automated logical reasoning. On the theoretical end, the course will cover widely-used logical theories and procedures for deciding the satisfiability of formulas in those theories. Topics will include propositional logic, first-order logic, linear arithmetic over reals and integers, theory of uninterpreted functions, bit-vector theory, and combinations of theories. On the practical end, the course will cover applications of logic in formal verification, theorem proving, and planning. Students will apply state-of-the-art automated reasoning tools to model and answer questions about complex systems.

Requisite: COSC-211. Spring semester. Professor Wu.

How to handle overenrollment: Priority to upper-level majors, then to other majors.

Students who enroll in this course will likely encounter and be expected to engage in the following intellectual skills, modes of learning, and assessment: quantitative work