Higher Order Proof Systems

高阶证明系统

• 批准号: 8705596
• 负责人: Dale Miller
• 金额: --
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 1987
• 资助国家: 美国
• 起止时间: 1987-08-15 至 1991-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8705596&HistoricalAwards=false
• 关键词: Higher; Order; Proof; Systems

This project will investigate the nature of computational systems which are meant to discover proofs and compute with them after they are discovered. The concept of proofs-as-values is not only interesting in its own right but also central for the development of interesting theorem provers and proof assistants for use by mathematicians and computer scientists. As a guide in designing such proof systems, several relevant issues in the semantics of constructive logics and higher-order polymorphic \-calculus will be investigated. A clear understanding of such models would help in developing a consistent and clean programming paradigm for the implementation of higher-order proof systems. The project will also investigate the role which extensions of logic programming languages could play as the underlying implementation languages for higher-order proof systems. The central role of search and equation solving (unification) in logic programming may make it more suitable for the implementation of proof systems than more traditionally used languages such as ML.

该项目将研究计算系统的本质，这些系统旨在发现证据并在发现证据后对其进行计算。 证明即值的概念不仅本身很有趣，而且对于开发供数学家和计算机科学家使用的有趣的定理证明器和证明助手也至关重要。 作为设计此类证明系统的指南，将研究构造逻辑和高阶多态微积分语义中的几个相关问题。 对此类模型的清晰理解将有助于为高阶证明系统的实现开发一致且干净的编程范例。 该项目还将研究逻辑编程语言的扩展作为高阶证明系统的底层实现语言所发挥的作用。 搜索和方程求解（统一）在逻辑编程中的核心作用可能使其比机器学习等更传统的语言更适合证明系统的实现。