Document Type
Article
Publication Date
2000
Publication Title
Annals of Mathematics and Artificial Intelligence
Volume
28
Issue
1
First Page
107
Last Page
126
Abstract
Generalization is a fundamental operation of inductive inference. While first order syntactic generalization (anti–unification) is well understood, its various extensions are often needed in applications. This paper discusses syntactic higher order generalization in a higher order language λ2 [1]. Based on the application ordering, we prove that least general generalization exists for any two terms and is unique up to renaming. An algorithm to compute the least general generalization is also presented. To illustrate its usefulness, we propose a program verification system based on higher order generalization that can reuse the proofs of similar programs.
Recommended Citation
Lu, Jianguo; Mylopoulos, John; Harao, Masateru; and Hagiya, Masami. (2000). Higher order generalization and its application in program verification. Annals of Mathematics and Artificial Intelligence, 28 (1), 107-126.
https://scholar.uwindsor.ca/computersciencepub/5
Comments
The article available for download is a preprint. The definitive version is published in the Annals of Mathematics and Artificial Intelligence and is available here. Copyright (2012) Springer.