Satisfiability Modulo Theory (SMT) is a paradigm of automated reasoning to tackle problems related to formulas containing both uninterpreted and interpreted symbols. Most SMT solvers are based on propositional satisfiability (SAT) conflict-driven clause-learning (CDCL) solvers, and they thus excel for combinatorial and shallow first-order reasoning, which make them most appropriate to tackle proof obligations stemming from verification tasks. Since more recently, SMT solvers are also used with success together with proof assistants to automatically discharge subgoals in formal proofs. Some SMT solvers provide precise proofs, so their usage does not jeopardize the assurance of proof correctness for machine assisted formal proofs.
In this talk, we will focus on one aspect of SMT solving, that is, quantifier reasoning. We will review the main techniques for instantiation. We will also briefly present the SMT-LIB input language, and future promising development in SMT, notably towards higher-order logic.
Copyright. All Rights Reserved.