Computer Science 690LG - Adv Logic in Computer Science

This course provides a rigorous introduction to mathematical logic from an algorithmic perspective. Topics include Propositional Logic: Horn Clause Satisfiability and SAT Solvers; First Order Logic: Soundness and Completeness of Resolution; Compactness Theorem; Automatic Theorem Proving; Model Checking. Students will learn the theory behind and use the following systems, languages, and tools: the Coq theorem prover, Datalog, the NuSMV Model Checker, and SAT and SMT solvers.

STUDENTS TAKING THIS COURSE SHOULD HAVE UNDERGRADUATE PREPARATION IN DISCRETE MATH AND ALGORITHMS. STUDENTS NEEDING SPECIAL PERMISSION MUST REQUEST OVERRIDES VIA THE ON-LINE FORM: https://www.cs.umass.edu/ugrad-education/course . MEETS WITH CMPSCI 513.