Lambda-Calculus, Type Theory, and Automated Theorem Proving

Lambda 微积分、类型论和自动定理证明

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

This research 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 which expresses the fundamental logical structure of the theorem, and then transform this into a 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 call 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.

这项研究涉及类型lambda演算中的自动定理证明和lambda演算的性质。类型化的lambda演算是一种高阶逻辑的公式，非常适合于数学和其他学科的形式化。Lambda演算既是一种逻辑理论，也是一种计算模型。它是高阶类型定理证明和函数式程序设计语言设计的基础。以往的研究表明，人们可以通过寻找表示定理基本逻辑结构的展开证明来寻找类型Lambda演算定理的证明，然后将其转化为自然演绎风格的证明。将继续研究寻找展开证明的方法、Lambda演算的各个方面以及相关的问题和问题。将继续开发现有的名为TPS的计算机化定理证明系统。它将被增强为一个实用和方便的工具，用于研究搜索扩展证明的方法，在扩展证明和自然演绎证明之间来回转换，以及交互、半自动和自动地构造和检查形式证明。