Computer Proofs of Limit Theorems
Proceedings of the Second International Joint Conference on Artificial Intelligence. Pages 586-599.
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 .
@inproceedings{ijcai1971p61,
title = {Computer Proofs of Limit Theorems},
author = {Bledsoe, W. W. and Boyer, Robert S. and Henneman, William H.},
booktitle = {Proceedings of the Second International Joint Conference on
Artificial Intelligence, {IJCAI-71}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {D.C. Cooper},
pages = {586--599},
year = {1971},
url = {https://ijcai.org/proceedings/1971/61},
}
TY - CPAPER TI - Computer Proofs of Limit Theorems AU - Bledsoe, W. W. AU - Boyer, Robert S. AU - Henneman, William H. T2 - Proceedings of the Second International Joint Conference on Artificial Intelligence, IJCAI-71 PB - International Joint Conferences on Artificial Intelligence PY - 1971 SP - 586 EP - 599 UR - https://ijcai.org/proceedings/1971/61 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
