Unification modulo an equality theory for equational logic programming

Logic in computer science (03B70) Equational classes, universal algebra in model theory (03C05) Logic programming (68N17) Grammars and rewriting systems (68Q42)

Review text

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.

Recommendations

Cites work

Cited in

(9)

This page was built for publication: Unification modulo an equality theory for equational logic programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2639627)