Higher-Order Equational Reasoning
Christian Prehofer · Birkhäuser Boston eBooks · 1998
This chapter introduces higher-order unification and term rewriting. First, Section 4.1 reviews a set of transformation rules for full higher-order pre-unification. This is followed by an important special case, higher-order patterns, where unification proceeds almost as in the first-order case. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.