Implementing rigid E-unification (Extended abstract)

M.G.J. Franssen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


    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.
    Original languageEnglish
    Title of host publicationInformal Proceedings of the 23rd International Workshop on Unification (UNIF 2009, Montreal, Canada, August 2, 2009)
    EditorsC. Lynch, P. Narendran
    Place of PublicationPotsdam NY, USA
    PublisherClarkson University
    Publication statusPublished - 2009


    Dive into the research topics of 'Implementing rigid E-unification (Extended abstract)'. Together they form a unique fingerprint.

    Cite this