Instantiation-based Methods for Equational Reasoning and Towards Theories Beyond

reasoning in first-order logic as instantiation-based methods
(IMs). Broadly speaking, unlike in traditional calculi such as
Resolution where the first-order satisfiability problem is tackled by
deriving logical conclusions, IMs attempt to reduce the first-order
satisfiability problem to propositional satisfiability by
intelligently instantiating clauses. Besides providing a proof
procedure which is in a way orthogonal to classical methods and can
complement those, IMs are naturally successful on problems which are
in effectively propositional logic or near-propositional logic. What
is more, IMs do perform well even in general first-order logic and by
virtue of the instantiation approach are able to build a bridge for
existing efficient ground reasoning modulo theories to cross over into
first-order reasoning.

The talk gives an overview of instantiation-based methods and recent
developments on the integration of equational reasoning. We then focus
on the Inst-Gen calculus, originally by Ganzinger and Korovin, and I
present our current results on the Inst-Gen method modulo equality
which has been implemented in the iProver-Eq system. In the end we
look at future directions to reasoning modulo theories in first-order
logic, which the Inst-Gen method is particularly well-suited to with
its modular combination of first-order and ground reasoning.

The talk is based on joint work with Konstantin Korovin at The
University of Manchester.