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.

Open to COMPSCI graduate students only. MEETS WITH CMPSCI 513. STUDENTS TAKING THIS COURSE SHOULD HAVE UNDERGRADUATE PREPARATION IN DISCRETE MATH AND ALGORITHMS. SEATS HELD FOR INCOMING STUDENT REGISTRATION. STUDENTS NEEDING SPECIAL PERMISSION MUST REQUEST OVERRIDES VIA THE ON-LINE FORM: https://www.cics.umass.edu/overrides.