Abstract
Logic has been one of the bedrocks of Computer Science since its earliest days, and hardly an area of the discipline has remained untouched by logic-based reasoning. Yet automating formal reasoning based on logic at scale has proved remarkably diUicult. A solver or decision procedure that looks promising in theory may fail to scale in practice, while an automated reasoning tool that performs impressively on real problems may oUer few mathematically rigorous or meaningful guarantees.
In this talk, I will discuss a few important problems in logical reasoning where theory and practice have informedand sometimes challengedeach other. This interplay has led to methods that scale to real-world problems, oUer rigorous and meaningful guarantees, and deepen our understanding of computation itself.
The choice of problems is necessarily shaped by my own interests and limitations. I will focus on propositional satisfiability solving, model counting, and functional synthesis, and conclude with some observations on the role of formal reasoning in the age of agentic AI.
Biodata of the Speaker
Supratik Chakraborty is Bajaj Group Chair Professor of Computer Science and Engineering at IIT Bombay, where he has been on the faculty since 2000. His research interests lie at the intersection of theoretical and applied formal methods, with a focus on developing logical reasoning algorithms with strong guarantees that also scale in practice. He is a Fellow of Indian National Academy of Engineering, a Distinguished Member of ACM, and a Distinguished Alumnus of IIT Kharagpur.
Rajaraman Lecture Series | Hari Sahasrabuddhe Lecture Series