Higher order generalization and its application in program verification

Generalization is a fundamental operation of inductive inference. While fir st order syntactic generalization (anti-unification) is well understood, it s various extensions are often needed in applications. This paper discusses syntactic higher order generalization in a higher order language lambda 2 [1]. Based on the application ordering, we prove that least general general ization exists for any two terms and is unique up to renaming. An algorithm to compute the least general generalization is also presented. To illustra te its usefulness, we propose a program verification system based on higher order generalization that can reuse the proofs of similar programs.