An Iterative and Bottom-up Procedure for Proving-by-Example
Abstract
We give a procedure for generalizing a proof of a concrete instance of a theorem by recovering inductions that have been expanded in the concrete proof. It consists of three operations introduction, extension and propagation , and by iterating these operations in a bottom-up fashion, it can reconstruct nested inductions. We discuss how to use EBG for identifying the induction formula, and how EBG must be modified so that nested inductions can be reconstructed.
Cite
Text
Hagiya. "An Iterative and Bottom-up Procedure for Proving-by-Example." European Conference on Machine Learning, 1993. doi:10.1007/3-540-56602-3_147Markdown
[Hagiya. "An Iterative and Bottom-up Procedure for Proving-by-Example." European Conference on Machine Learning, 1993.](https://mlanthology.org/ecmlpkdd/1993/hagiya1993ecml-iterative/) doi:10.1007/3-540-56602-3_147BibTeX
@inproceedings{hagiya1993ecml-iterative,
title = {{An Iterative and Bottom-up Procedure for Proving-by-Example}},
author = {Hagiya, Masami},
booktitle = {European Conference on Machine Learning},
year = {1993},
pages = {336-341},
doi = {10.1007/3-540-56602-3_147},
url = {https://mlanthology.org/ecmlpkdd/1993/hagiya1993ecml-iterative/}
}