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 lq*, which IS a (nonstandard) extension of the real field ~R containing "infinitesimals" and "infinitely large numbers " A theorem T about 1R 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 infinitesi- mals 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 continu- ous, and some theorems about sequences