Lambda-Calculus, Type Theory, and Autmated Theorem Proving

点击翻译按钮获取中文摘要

This investigation is concerned with automated theorem proving in the typed lambda calculus and with properties of the lambda calculus. The typed lambda calculus is a formulation of higher-order logic well suited to the formalization of mathematics and other disciplines. The lambda calculus is both a logical theory and a model of computation. It is fundamental to both higher-type theorem proving and functional programming language design. Previous research has shown that one can search for a proof of a theorem of typed lambda calculus by searching for an expansion proof in natural deduction style. Research will continue on methods for finding expansion proofs, on various aspects of the lambda calculus, and on related problems and questions. Development of an existing computerized theorem proving system called TPS will continue. It will be enhanced as a practical and convenient tool for investigating methods of searching for expansion proofs, translating back and forth between expansion proofs and natural deduction proofs, and constructing and checking formal proofs interactively, semi-automatically, and automatically.