Structure vs. Invariants in Proofs (StrIP)

所有的数字都是偶数或奇数。但为什么呢？我该如何证明这一点呢？一种方法是注意到每次我们加1时一个数字的奇偶性都会翻转，另一种方法是只检查最后一位数字。这两个“证明”都引出了一个“算法”来检查一个数是偶数还是奇数。然而，在后一种情况下，该算法的效率呈指数级提高，我们只需要查看一个数字，而不是从头开始生成整个数字。这样我们就可以说这两个证明是真正不同的。在最抽象的层面上，“证明中的结构与不变量”（StrIP）关注的是两个证明不同或相同时的理解。这是一个可以追溯到世纪早期的证明论问题，通常被称为希尔伯特第24问题。虽然这是一个基本的理论问题，但希尔伯特第24问题和随后的证明理论努力是现代计算机科学的许多方面的基础，例如编程语言理论和可计算性理论。特别是，证明理论是形式验证的基础支柱之一。这是一个新兴的领域，使我们能够经常 * 保证 * 软件正确运行，并将成为越来越相关的认证软件在真实的世界。然而，仍然有一个根本的障碍，解决希尔伯特的第24个问题：归纳推理。“归纳法”是一种强大的证明技术，在数学和计算机科学中不可或缺;它允许我们通过首先证明P（0）然后证明P（x）总是蕴涵P（x+1）来证明所有数x的性质P（x）。这就像一个无限的多米诺骨牌序列：如果我打翻了第一个，其他所有的最终都会倒下。在计算方面，归纳的证明论处理是一个必要的，以便对一般的计算机程序进行推理。StrIP的目标是通过“循环证明”的概念对归纳进行全面的处理。这是在过去20-30年中出现在计算逻辑中的一种现象，它允许我们以有限的方式将归纳法分解为更精细的计算步骤。通过将其与证明理论中的其他最新思想相结合，即所谓的“深度推理”，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.