Higher-order equational unification via explicit substitutions. (English) Zbl 0888.03007

Hanus, Michael (ed.) et al., Algebraic and logic programming. 6th international joint conference, ALP ’97 - HOA ’97, Southampton, GB, September 3–5, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1298, 61-75 (1997).
The authors show how to perform the higher-order \(E\)-unification problem as a first-order unification problem via a union of two equational theories including \(E\) and a calculus of explicit substitution. A rule-based unification procedure is described. This procedure extends the results of G. Dowek, T. Hardin and C. Kirchner who showed how to reduce the higher-order unification problem to a first-order unification problem modulo a first-order theory of explicit substitution.
For the entire collection see [Zbl 0871.00033].
Reviewer: N.Zamov (Kazan’)


03B40 Combinatory logic and lambda calculus
68Q42 Grammars and rewriting systems