Free Variables and Theories: Revisiting Rigid E-unification

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.