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  for practical situations where many similar rigid E-unification problems have to be solved. We implement the methods of Comon  and Nieuwenhuis  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.
|Title of host publication||Informal Proceedings of the 23rd International Workshop on Unification (UNIF 2009, Montreal, Canada, August 2, 2009)|
|Editors||C. Lynch, P. Narendran|
|Place of Publication||Potsdam NY, USA|
|Publication status||Published - 2009|