Course 6.S095: Automated Reasoning in AI
MIT IAP 2017
Lecturer: Sicun Gao
Time: 2pm to 3pm, Jan-13 to Jan-24 (working days), 2017
Join the google group for the course to receive notices.
Automated reasoning is an area of AI that studies algorithmic approaches to logical reasoning, and problem solving in general. It is the oldest branch and also the next frontier of AI, thanks to tremendous progress in recent decades. The course will first cover the basics of propositional and first-order logic, and then focus on core reasoning algorithms and their connections to standard topics in AI, including search, learning, planning, and optimization.
- Jan-13: Propositional and first-order logic
- Jan-17: Getting started as users of automated reasoning tools z3 and dReal (installation,
- Jan-18: SAT solving and combinatorial search
- Jan-19: Numerical constraint solving and optimization
- Jan-20: Guest lecture on applications of reasoning systems in safe autonomous driving
- Jan-23: Theoretical foundations and future research directions
- Jan-24 (or some later date): Student project presentation
Familiarity with C++. Calculus and linear algebra.
Lecture notes, and chapters from "Artificial Intelligence: A Modern Approach" and "Handbook of Satisfiability," will be provided.
Students will be required to turn in 6-page reports for their course projects (in AAAI/IJCAI paper formats). The goal is to guide students to find interesting research topics (applications, algorithms, or theory) and initiate some publishable line of work. No final exam.