Higher Order Proof Systems

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

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.