SMT- Quantifiers, and Future Prospects - IPAM at UCLA

Delve into the world of Satisfiability Modulo Theory (SMT) and its applications in automated reasoning through this informative lecture. Explore the foundations of SMT solvers, their relationship with propositional satisfiability (SAT) and conflict-driven clause-learning (CDCL) solvers, and their effectiveness in combinatorial and shallow first-order reasoning. Discover how SMT solvers are utilized in verification tasks and in conjunction with proof assistants for formal proofs. Focus on quantifier reasoning techniques, particularly instantiation methods, and gain insights into the SMT-LIB input language. Conclude with an overview of promising future developments in SMT, including advancements towards higher-order logic.