Recent Advances in Instantiation-Based First-Order Reasoning

Konstantin Korovin

Instantiation-based automated reasoning aims at utilising
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 smart generation of
instances with satisfiability checking of ground
formulas. Instantiation-based methods particularly excel in reasoning
in the effectively propositional fragment (EPR) of first-order logic,
also called Bernays-Scheonfinkel-Ramsey fragment.  It turns out that a
number of problems such as bounded model checking, finite model
finding, planning and satisfiability of quantified Boolean formulas
can be naturally encoded into the EPR fragment.  This opens a wide
range of applications for instantiation-based methods. In this talk I
will overview the recent developments in instantiation-based
reasoning, focusing on a modular approach that we have been
developing. I will also discuss applications of instantiation-based
reasoning in bounded model checking and finite model finding.