---
title: "Computer Proofs of Limit Theorems"
authors:
  - "W. W. Bledsoe"
  - "Robert S. Boyer"
  - "William H. Henneman"
doi: ""
url: "https://ijcai.org/proceedings/1971/61"
pdf: "https://ijcai.org/proceedings/1971/0061.pdf"
venue: "Proceedings of the Second International Joint Conference on Artificial Intelligence"
year: 1971
pages: "586-599"
track: ""
keywords:
---

# Computer Proofs of Limit Theorems

W. W. Bledsoe, Robert S. Boyer, William H. Henneman

*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 .