This research is concerned with automated theorem proving in type theory, which is also known as higher-order logic. The basic purpose of this research is to automate and facilitate the use of rigorous logic. Rigorous reasoning plays (or should play) an important role in a wide variety of intellectual endeavors, and computerized systems which facilitate the use of logic have many important potential applications. The focus of this research is on proving theorems of a formulation of higher- order logic known as the typed lambda-calculus. This formal language includes first-order logic, but in a practical sense it has greater expressive power, and it is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. Part of this research involves continued development of an existing computerized theorem proving system called TPS, which can be used to construct and check formal proofs (in natural deduction style) interactively, semi-automatically, and automatically. In automatic mode, TPS first searches for an expansion proof, which expresses in a nonredundant way the fundamental logical structure of proofs of the theorem in a variety of styles, and then transforms this into a proof in natural deduction style. The interactive commands for applying rules of inference are available in a related program called ETPS (Educational Theorem Proving System), which is used interactively by students in logic courses to construct natural deduction proofs. The possibility of using TPS in a mixture of automatic and interactive modes makes it an attractive tool for working on complex logical problems in a variety of disciplines. Research will continue on methods of searching for expansion proofs, higher-order unification, methods of translating back and forth between expansion proofs and natural deduction proofs, improved presentations of proofs, enhancement of TPS as a useful logical tool, and related problems and questions.
