Unification modulo an equality theory for equational logic programming (Q2639627)

Attempts to combine logic- and functional programming have led to the problem of unification relative to an equational theory - the E- unification problem. This problem in general can not be completely solved; moreover, if the problem can be solved a finite minimal set of solutions may fail to exist. In order to cope with these difficulties researchers introduce more restricted tests for equality to be used within narrowing strategies, which do preserve however the effectivity and feasibility of the unification procedure within logic programming. The above problem area is investigated with the purpose of combining O'Donnell's equational programming style (based on term-rewriting technology) with logic programming. The authors present techniques yielding narrowing strategies which deliver complete and minimal sets of solutions with the property that the equality theory used still captures the intended notion of equational programming in the original language.