CS 433 : Automated Reasoning 2020

Instructor : Ashutosh Gupta

Mode of instruction : weakly release of recorded videos and slides
Interactive session : Once a week we will have an iterective session followed by an online quiz

The course is about the design and implementation of solvers for proving/disproving validity of statements in various logics. The solvers are often referred as reasoning engines, hence the course name automated reasoning. The reasoning problems are inherently hard and there are no known provably efficient algorithms for them. However, we may have efficient heuristics that may solve some interesting and important instances of the problems. In the last three decades, automated reasoning has risen to be a matured and an effective technology that can be applied to the reasoning problems arising from a wide range of fields.

The course will cover five major topics: satisfiability solvers, satisfiability modulo theories solvers, decision procedures (theories), interactive theorem provers, and first order logic solvers. In each part, we will discuss encoding the problems of interest into the reasoning problems, the efficient heuristics, the implementation issues of the heuristics, and their theoretical understanding. The course will include programming assignments/projects.

Source material

Self-learning backrgound material


  • Please install Z3 and its python interface before second week/li>

    Evaluation structure

    The presentations will be distributed over the semester. The topics and slots will be floated time to time on this website. A schedule of presentation will be announced in the 3rd week of the class.



    Last modified: ()