Automated Theorem in Proving in Type Theory

这项研究涉及类型理论中的自动定理证明，也被称为高阶逻辑。这项研究的基本目的是自动化和促进严格逻辑的使用。严格的推理在各种各样的智力活动中扮演着(或应该扮演)重要的角色，而便于使用逻辑的计算机化系统有许多重要的潜在应用。这项研究的重点是证明一种高阶逻辑的公式，称为类型化的Lambda演算。这种形式化语言包括一阶逻辑，但在实际意义上它具有更强的表达能力，特别适合于数学和其他学科的形式化以及硬件和软件的指定和验证。这项研究的一部分涉及继续开发现有的计算机化定理证明系统TPS，该系统可用于交互、半自动和自动地构造和检查形式证明(以自然演绎方式)。在自动模式下，TPS首先搜索以非冗余方式表示定理证明的基本逻辑结构的扩展证明，然后将其转换为自然演绎风格的证明。应用推理规则的交互命令可在一个相关程序ETPS(教育定理证明系统)中获得，该程序供学生在逻辑课程中交互使用，以构建自然演绎证明。TPS可以在自动模式和交互模式的混合模式下使用，这使它成为处理各种学科中复杂逻辑问题的一个有吸引力的工具。将继续研究寻找扩展证明的方法，高阶统一，在扩展证明和自然演绎证明之间来回转换的方法，改进证明的呈现，增强TPS作为有用的逻辑工具，以及相关的问题和问题。

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.