Higher-order unification revisited: Complete sets of transformations (Q1823936)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Higher-order unification revisited: Complete sets of transformations |
scientific article |
Statements
Higher-order unification revisited: Complete sets of transformations (English)
0 references
1989
0 references
Some approach to higher-order unification is presented. The approach is based on the method of transformation of terms and extends the approach developed by Martelli and Montanari in the context of first-order unification. The method of transformations for solving unification problems is much like the well-known Gaussian method used for solving systems of linear equations. Gaussian elimination and first-order unification are somewhat similar. But in the higher-order case the analogy breaks down. The most important differences to the first-order case have to do with the imitation rule and the generalization of the notion of a partial binding to higher-order substitutions.
0 references
simple theory of types
0 references
generalization of partial binding to higher-order substitutions
0 references
higher-order unification
0 references
method of transformations
0 references
imitation rule
0 references
0 references