Automated Theorem Proving in Type Theory

本研究的基本目的是自动化和促进严格逻辑的使用。严格推理在各种各样的智力活动中扮演（或应该扮演）重要的角色，自动推理工具有许多重要的潜在应用。证明定理的过程将是自动推理工具的关键组成部分，因为这些过程可以用作推理机制。这项研究的重点是证明被称为类型理论的高阶逻辑公式的定理（更具体地说，是类型化的λ演算）。这种形式语言包括一阶逻辑，但在实际意义上，它具有更强的表达能力，并且特别适合于数学和其他学科的形式化，以及指定和验证硬件和软件。这项研究的一部分涉及继续发展现有的计算机化定理证明系统，称为TPS，该系统可用于交互式，半自动和自动地构建和检查形式证明（以自然演绎风格）。在自动模式下，TPS首先寻找一个展开式证明，以一种非冗余的方式表达定理各种形式证明的基本逻辑结构，然后将其转化为一个自然演绎形式的证明。应用推理规则的交互式命令可在相关的程序中获得，称为ETPS（教育定理证明系统），学生在逻辑课程中交互式地使用它来构建自然演绎证明。在自动和交互模式的混合中使用TPS的可能性使其成为处理各种学科中复杂逻辑问题的有吸引力的工具。更多关于TPS的信息可以在http://gtps.math.cmu.edu/tps.html上找到。研究了寻找展开式证明的方法，包括寻找集合变量的适当替换方法、寻找子公式的匹配方法以及它们之间的相互作用；对证据的表述、篡改、展示和翻译；加强TPS作为有用的逻辑工具；以及相关的问题。

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 automated reasoning tools have many important potential applications. Procedures for proving theorems will be crucial components of automated reasoning tools, since these procedures can be used as inference mechanisms. The focus of this research is on proving theorems of a formulation of higher-order logic known as type theory (more specifically, 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 non-redundant 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. More information about TPS can be found at http://gtps.math.cmu.edu/tps.html. The research involves methods of searching for expansion proofs, including methods of finding appropriate substitutions for set variables, methods of searching for matings of subformulas, and the interactions between these; representations, manipulations, presentations, and translations of proofs; enhancement of TPS as a useful logical tool; and related problems and questions.