Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques

Abstract

A procedure has been developed for automatically proving theorems in analysts by using the methods of nonstandard analysis This procedure utlhzes the field IR*, which IS a (nonstandard) extension of the real field IR containing “infinitesimals” and “infinitely large numbers” A theorem T about IR is valid if and only If ItS corresponding form T* Is vahd about IR* A given theorem T is (automatically) converted to T* and proved in this new setting, which is particularly well suited for automatic proofs The conversion to T* is obtained by using the nonstandard definitions of terms such as “continuous,” “compact,” and “accumulation point” An existing prover has been slightly altered to carry out these proofs. The concepts of typing, reduction (rewrite rules), algebraic simplification, and controlled forward chaining play major roles in handhng infinitesimals and other typed quantities A computer program has proved several theorems in analysis including the Bolzano-Weierstrass theorem, the theorem that a continuous function on a compact set is umformly continuous, and some theorems about sequences. © 1977, ACM. All rights reserved.