Automated Theorem Proving in Type Theory

类型论中的自动定理证明

• 批准号: 9624683
• 负责人: Peter Andrews
• 金额: $ 13.14万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-08-15 至 1999-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9624683&HistoricalAwards=false
• 关键词: Automated; Theorem; Proving; Type; Theory

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, methods of translating back and forth between expansion proofs and natural deduction proofs, on higher-order unification, on enhancement of TPS as a useful logical tool, and on related problems and question s. ***

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