Implementing rigid E-unification (Extended abstract)

M.G.J. Franssen

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer 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.
    Originele taal-2Engels
    TitelInformal Proceedings of the 23rd International Workshop on Unification (UNIF 2009, Montreal, Canada, August 2, 2009)
    RedacteurenC. Lynch, P. Narendran
    Plaats van productiePotsdam NY, USA
    UitgeverijClarkson University
    StatusGepubliceerd - 2009


    Duik in de onderzoeksthema's van 'Implementing rigid E-unification (Extended abstract)'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit