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.