Higher-order critical pairs

A subclass of λ-terms, called patterns, which have unification properties resembling those of first-order terms, is introduced. Higher-order rewrite systems are defined to be rewrite systems over λ-terms whose left-hand sides are patterns: this guarantees that the rewrite relation is easily computable. The notion of critical pair is generalized to higher-order rewrite systems, and the analog of the critical pair lemma is proved. The restricted nature of patterns is instrumental in obtaining these results. The critical pair lemma is applied to a number of λ-calculi and some first-order logic formalized by higher-order rewrite systems