Automated Reasoning and Program Verification



  • 2016 Spring/Summer (Jan - May)

This is an introductory course for mathematical logic. In the course, we will cover propositional logic, first-order logic, logical theories, and (un)decidablity of various theories. Most of the course is about the theoretical foundation of logic. Additionally, we will use SAT solvers, first order provers, and assisted theorem provers for some hands on experience.