Implementing rigid E-unification (Extended abstract)

Rigid E-unification problems arise naturally in automated theorem provers that deal with equality. In this paper we discuss how to implement a rigid E-unifier, focussing on efficiency. We improve the algorithm to compute rigid E-unifiers as proposed by Degtyarev and Voronkov [4] for practical situations where many similar rigid E-unification problems have to be solved. We implement the methods of Comon [1] and Nieuwenhuis [8] to solve symbolic ordering constraints generated by the algorithm. We compute solved forms of constraints without storing intermediate results and without performing any substitutions. Instead of computing an exponential number of simple systems for each solved form, we build a graph from the solved form such that a bounded back-tracking algorithm can search for a satisfiable simple system without the need to generate them all.