著者

萩谷 昌己

出版者

社団法人人工知能学会

雑誌

人工知能学会誌 (ISSN:09128085)

巻号頁・発行日

vol.6, no.3, pp.388-396, 1991-05-01

被引用文献数

1

---

The problem of generalizing explanations or proofs have been studied in the field of explanation-based learning. In this paper, we discuss the use of higher-order unification for solving the problem. We first point out that the problem of generalizing a proof by replacing constant terms with variables can be considered as a matching problem in higher-order type theory, and higher-order unification for terms representing proofs can solve the problem. This method of generalizing a proof has the advantage that it can be naturally extended to cope with the problem of generalizing a proof by introducing induction, also known as the problem of generalizing number. We also discuss the use of recursively reducibility for generalizing equational proofs, particularly computational traces of functions.