Implementing rigid e-unification
Mgj Michael Franssen · TU/e Research Portal · 2008
Rigid E-unification problems arise naturally in automated theorem provers that deal with equality.While there is a lot of theory about rigid E-unification, only few implementations exist.Since the problem is NPcomplete, direct implementations of the theory are slow.In this paper we discuss how to implement a rigid E-unifier, focussing on efficiency.First, we introduce an efficient representation of unifying substitutions to implement a regular Robinson unification algorithm.Next, we discuss the algorithm to compute rigid E-unifiers as proposed by Degtyarev et al. [4] and we discuss how to solve the symbolic ordering constraint as proposed by Comon [1] and Nieuwenhuis [10].Finally, we discuss how rigid E-unification can be implemented efficiently.However, the worst case is still exponential.