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 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 KEY WORDS AND PHRASES theorem proving, natural deduction, nonstandard analysis, analysis, database

This paper is an initial progress report on the development of an interactive system for verifying that computer programs meet given formal specifications. The system is based on the conventional inductive assertion method: given a program and its specifications, the object is to generate the verification conditions, simplify them, and prove what remains. The important feature of the system is that the human user has the opportunity and obligation to help actively in the simplifying and proving. A general description is given of the overall design philosophy, structure, and functional components of the system, and a simple sorting program is used to illustrate both the behavior of major system components and the type of user interaction the system provides.

A new technique is given for establishing the completeness of resolution-based deductive systems for first-order logic (with or without equality) and several new completeness results are proved using this technique. The technique leads to very simple and clear completeness proofs and can be used to establish the completeness of most resolution-based deductive systems reported in the literature. The main new result obtained by means of this technique is that a linear format for resolution with merging and set of support and with several further restrictions is a complete deductive system for the first-order predicate calculus.

Some problems arising in multicategory (many pattern types) pattern recognition are treated mathematically, and formulas are derived which describe some inherent limitations associated therewith. The principal results concern the “dimensional” and “correlational” effects and their degradation of a multimeasurement recognition system.

It is shown that a previous version of the n-tuple pattern recognition method can be made more effective by making certain changes in the learning phase. A means of further increasing readability through judicious choice of n-tuples is described.