Invited Talk: Konstantin Korovin

Instantiation-based automated reasoning aims to utilise industrial-strength SAT and SMT technologies in the more general context of first-order logic. The basic idea behind instantiation-based reasoning is to combine clever generation of instances with satisfiability checking of ground formulae.

There are a number of challenges arising in this area ranging from theoretical issues such completeness, integration of theories and decidable fragments to efficient implementation: inference strategies, indexing and redundancy elimination. In this talk I will overview the recent advances in instantiation-based reasoning, focusing on a modular approach which allows us to use off-the-shelf SAT and SMT solvers for ground formulae as part of general first-order reasoning.