The efficient integration of theory reasoning in first-order calculi
with free variables (such as sequent calculi or tableaux) is a
long-standing challenge. For the case of the theory of equality, an
approach that has been extensively studied in the 90s is rigid
E-unification, a variant of equational unification in which the
assumption is made that every variable denotes exactly one term
(rigid semantics). The fact that simultaneous rigid E-unification is
undecidable, however, has hampered practical adoption of the method,
and today there are few theorem provers that use rigid
E-unification.
One solution is to consider incomplete algorithms for computing
(simultaneous) rigid E-unifiers, which can still be sufficient to
create sound and complete theorem provers for first-order logic with
equality; such algorithms include rigid basic superposition proposed
by Degtyarev and Voronkov, but also the much older subterm
instantiation approach introduced by Kanger in 1963 (later also
termed minus-normalisation). We introduce bounded rigid E-unification (BREU)
as a new variant of E-unification corresponding to subterm instantiation. In
contrast to general rigid E-unification, BREU is NP-complete for
individual and simultaneous unification problems, and can be solved
efficiently with the help of SAT; BREU can be combined with
techniques like congruence closure for ground reasoning, and be used
to construct theorem provers that are competitive with
state-of-the-art tableau systems. We outline ongoing research how
BREU can be generalised to other theories than equality.