Structure vs. Invariants in Proofs (StrIP)

证明中的结构与不变量 (StrIP)

基本信息

批准号：
MR/S035540/1
负责人：
Anupam Das
金额：
$ 151.45万
依托单位：
University of Birmingham
依托单位国家：
英国
项目类别：
Fellowship
财政年份：
2020
资助国家：
英国
起止时间：
2020 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=MR%2FS035540%2F1
关键词：
Structure vs.Invariants Proofs StrIP

项目摘要

All numbers are even or odd. But why? How could I prove this *formally*? One way is to notice that the parity of a number flips every time we add 1, another way is to just check the last digit. Both of these 'proofs' induce an 'algorithm' for checking whether a number is even or odd. However in the latter case the algorithm is exponentially more efficient, - we only need to look at one digit rather than generate the entire number from scratch. In this way we can say that the two proofs are really *different*.'Structure vs. Invariants in Proofs' (StrIP), at its most abstract level, is concerned with understanding when two proofs are different or the same. This is a question in proof theory that can be traced back to the early 20th century, and is often known as Hilbert's 24th problem. While it is a fundamentally theoretical question, Hilbert's 24th problem and the proof theoretic endeavours that have followed underlie many aspects of modern computer science, such as programming language theory and computability theory. In particular, proof theory is one of the foundational pillars of Formal Verification. This is an emerging field that allows us to often *guarantee* that software functions correctly, and is set to become increasingly relevant for certifying software in the real world.However, there remains one fundamental barrier to resolving Hilbert's 24th problem: inductive reasoning. 'Induction' is a powerful proof technique that is indispensable in mathematics and computer science; it allows us to prove a property P(x) for all numbers x by first proving P(0) then proving that P(x) always implies P(x+1). It is like an infinite sequence of dominoes: if I knock over the first one, every other one will eventually fall. On the computing side, a proof theoretic treatment of induction is a necessity in order to reason about general computer programs.The goal of StrIP is to give a comprehensive treatment of induction via the notion of 'cyclic proofs'. This is a phenomenon that has emerged in computational logic over the last 20-30 years and allows us to decompose induction into finer computational steps in a finitary way. By combining this with other recent ideas in proof theory, so-called 'Deep Inference', StrIP will build a bridge between two of the most important subjects in theoretical computer science: proof theory and automata theory. Ultimately, the goal is to apply the techniques developed to Automated Reasoning via concrete implementations, and more generally to the automated verification of computer programs.

所有数字都是偶数或奇怪的。但为什么？我该如何证明 *正式 *？一种方法是注意一个数字的奇偶校验每次添加1时都会翻转，另一种方法是检查最后一个数字。这两个“证明”都诱导了一个“算法”，用于检查一个数字是偶数还是奇怪。但是，在后一种情况下，该算法呈指数效率，我们只需要查看一个数字，而不是从头开始生成整个数字。通过这种方式，我们可以说这两个证据确实是 *不同的 *。“结构与证明中的不变”（最抽象的层面）与理解何时两个证明是不同或相同的何时了解。这是一个证明理论中的问题，可以追溯到20世纪初，通常被称为希尔伯特的第24个问题。虽然这是一个从根本上说的理论问题，但希尔伯特的第24个问题以及遵循现代计算机科学许多方面的基础的证据理论努力，例如编程语言理论和可计算理论。特别是，证明理论是正式验证的基本支柱之一。这是一个新兴领域，使我们经常 *保证 *该软件正确地运行，并且将对在现实世界中的认证软件变得越来越重要。但是，仍然存在一个解决希尔伯特的第24个问题的基本障碍：感应推理。 “归纳”是一种有力的证明技术，在数学和计算机科学中是必不可少的。它允许我们先证明P（0）证明所有数字X的属性P（X），然后证明P（X）总是暗示P（X+1）。这就像一个无限的多米诺骨牌序列：如果我敲开第一个，每一个最终都会掉下来。在计算方面，为了推理一般计算机程序，对诱导的理论治疗是必要的。条带的目的是通过“循环证明”的概念对归纳进行全面处理。在过去的20 - 30年中，这是一种在计算逻辑中出现的现象，使我们能够以一种限制的方式将归纳分解为更精细的计算步骤。通过将其与所谓的“深度推论”中的其他最新思想相结合，Strip将在理论计算机科学中最重要的两个主题之间建立桥梁：证明理论和自动机理论。最终，目标是将开发的技术应用于通过具体实现的自动推理，更普遍地应用于计算机程序的自动验证。