A Typed Lambda-Calculus for Proving-by-Example and Bottom-up Generalization Procedure
Abstract
A generalization procedure which reconstructs mathematical inductions that are expanded in a proof of an example is formulated under a typed λ-calculus that is designed for increasing the applicability of the procedure. The λ-calculus, an extension of Logical Framework, allows recursions and inductions on natural numbers, and inferences on linear arithmetical terms are built into its type system. The generalization procedure is iterated in a bottom-up fashion to construct nested inductions. Consequently, it can also find inductions whose induction formula is a limited form of bounded quantification.
Cite
Text
Hagiya. "A Typed Lambda-Calculus for Proving-by-Example and Bottom-up Generalization Procedure." International Conference on Algorithmic Learning Theory, 1993. doi:10.1007/3-540-57370-4_38Markdown
[Hagiya. "A Typed Lambda-Calculus for Proving-by-Example and Bottom-up Generalization Procedure." International Conference on Algorithmic Learning Theory, 1993.](https://mlanthology.org/alt/1993/hagiya1993alt-typed/) doi:10.1007/3-540-57370-4_38BibTeX
@inproceedings{hagiya1993alt-typed,
title = {{A Typed Lambda-Calculus for Proving-by-Example and Bottom-up Generalization Procedure}},
author = {Hagiya, Masami},
booktitle = {International Conference on Algorithmic Learning Theory},
year = {1993},
pages = {73-86},
doi = {10.1007/3-540-57370-4_38},
url = {https://mlanthology.org/alt/1993/hagiya1993alt-typed/}
}