Advanced Topics in Logic: Automated Reasoning and Satisfiability Course ID 15816 Doctoral Breadth Course: Programming Languages - (*) Classes marked with "*" (star) are appropriate for any CSD doctoral or 5th year master's student. Description Automated reasoning has become a powerful technology with applications ranging from verification of hardware and software to solving long-standing open problems in mathematics. This course covers several state-of-the-art automated reasoning techniques and provides hands-on experience with research questions in this area. Key Topics Automated reasoning Propositional logic Satisfiability modulo theories Verification Proof complexity Encoding Certifying programs Learning Resources Slides notes will be posted, and videos of the Fall'21 lectures are available. Course Relevance All levels are welcome Course Goals Along the way, students will learn how to: - Represent problems in a suitable logic; - Use, modify, and develop automated reasoning tools; - Produce, optimize, and verify proofs; and - Write a scientific paper. Pre-required Knowledge This is an introductory graduate course with no formal prerequisites. Assessment Structure Grades are based on three homework assignments (15% × 3 = 45%), final project (45%), and participation (10%). The final project should raise novel research questions and provide some nontrivial answers. These projects should be described in a report and presented in class at the end of the semester. Course Link https://www.cs.cmu.edu/~mheule/15816-f23/
