Lambda-Calculus, Type Theory, and Autmated Theorem Proving

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

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

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.

本研究关注的是自动定理证明在 类型lambda演算和lambda演算的属性。 的 类型lambda演算是高阶逻辑的一种形式， 适合于数学和其他学科的形式化。 的 lambda演算既是一种逻辑理论，也是一种计算模型。 它是基本的两个高型定理证明和功能 编程语言设计 以前的研究表明，人们可以搜索一个证明， 类型lambda演算定理的展开式证明 用自然推理的方式。 将继续研究 在lambda演算的各个方面找到扩展证明， 以及有关的问题。 开发了一个现有的计算机化定理证明系统， TPS将继续。 它将被增强为一种实用和方便的 用于调查搜索扩展证明的方法的工具， 在扩展证明和自然证明之间来回转换 演绎证明，构造和检验形式证明 交互地、半自动地和自动地。