Structure vs Invariants in Proofs (StrIP)

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

• 批准号: MR/Y011716/1
• 负责人: Anupam Das
• 金额: $ 75.78万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2024
• 资助国家: 英国
• 起止时间: 2024 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=MR%2FY011716%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 时数字的奇偶校验都会翻转，另一种方法是仅检查最后一位数字。这两个“证明”都引出了一种检查数字是偶数还是奇数的“算法”。然而，在后一种情况下，算法的效率呈指数级提高， - 我们只需要查看一个数字，而不是从头开始生成整个数字。通过这种方式，我们可以说这两个证明确实是“不同的”。“证明中的结构与不变量”（StrIP）在其最抽象的层面上涉及理解两个证明何时不同或相同。这是证明论中的一个问题，可以追溯到20世纪初，通常被称为希尔伯特第24问题。虽然这是一个根本性的理论问题，但希尔伯特的第 24 个问题和随后的证明理论努力奠定了现代计算机科学许多方面的基础，例如编程语言理论和可计算性理论。特别是，证明理论是形式验证的基本支柱之一。这是一个新兴领域，它使我们能够经常“保证”软件正确运行，并且与现实世界中的软件认证变得越来越相关。然而，解决希尔伯特第 24 个问题仍然存在一个根本障碍：归纳推理。 “归纳法”是数学和计算机科学中不可或缺的强大证明技术；它允许我们通过首先证明 P(0) 然后证明 P(x) 总是蕴涵 P(x+1) 来证明所有数字 x 的属性 P(x)。这就像一个无限序列的多米诺骨牌：如果我推倒第一张，那么其他所有的最终都会倒下。在计算方面，为了推理一般计算机程序，归纳法的证明理论处理是必要的。StrIP 的目标是通过“循环证明”的概念对归纳法进行全面的处理。这是过去 20-30 年来计算逻辑中出现的一种现象，它使我们能够以有限的方式将归纳法分解为更精细的计算步骤。通过将其与证明理论中的其他最新思想（即所谓的“深度推理”）相结合，StrIP 将在理论计算机科学中两个最重要的主题：证明理论和自动机理论之间架起一座桥梁。最终的目标是通过具体实现将开发的技术应用于自动推理，更广泛地应用于计算机程序的自动验证。