Computer Proofs of Limit Theorems
Abstract
Some relatively simple concepts have been developed which, when incorporated into existing automatic theorem proving programs (including those using resolution), enable them to prove efficiently a number of the limit theorems of elementary calculus, including the theorem that differentiable functions are continuous. These concepts include: (1) A limited theory of types, to designate whether a given variable belongs to a certain interval on the real line, (2) An algebraic simplification routine, (3) A routine for solving linear inequalities, applicable to all areas of analysis, and (4) A “limit heuristic”, designed especially for the limit theorems of calculus.
Cite
Text
Bledsoe et al. "Computer Proofs of Limit Theorems." International Joint Conference on Artificial Intelligence, 1971. doi:10.1016/0004-3702(72)90041-0Markdown
[Bledsoe et al. "Computer Proofs of Limit Theorems." International Joint Conference on Artificial Intelligence, 1971.](https://mlanthology.org/ijcai/1971/bledsoe1971ijcai-computer/) doi:10.1016/0004-3702(72)90041-0BibTeX
@inproceedings{bledsoe1971ijcai-computer,
title = {{Computer Proofs of Limit Theorems}},
author = {Bledsoe, W. W. and Boyer, Robert S. and Henneman, William H.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1971},
pages = {586-600},
doi = {10.1016/0004-3702(72)90041-0},
url = {https://mlanthology.org/ijcai/1971/bledsoe1971ijcai-computer/}
}