Complexity and Non-determinism in Deep Inference

证明论和证明复杂性研究数学和理论计算机科学中的形式证明。诉诸正式的证明是我们不犯错误的最好机会。形式证明是相对简单和清晰的对象，无论是人类还是计算机都可以以极高的置信度进行验证。计算机在我们的生活中扮演着重要的角色：我们的安全和我们的商品的安全，取决于它们可靠和安全的行为。我们都知道，计算机系统的安全不断受到挑战，我们对维护计算机系统受控的一些最大希望是开发基于正式证明的计算机语言和验证工具。这促使人们对形式证明的兴趣从数学转向理论计算机科学。与数学相比，计算机科学更关注的是定量问题，比如我们证明定理的效率。例如，著名的P vs NP问题与定理证明直接相关，既属于证明论，又属于证明复杂性。六年前，该提案的PI与申请资金的RA以及他的学生和同事一起发起了一项关于证明论中一种新的方法论的研究计划，称为深度推理。深度推理以一种比以前更接近计算机科学的方式看待形式证明，因为它以一种原则上比传统方法更有效的方式利用了它们的信息内容。为了将深度推理确立为证明理论领域的一个适当领域，我们设计了证明系统，并开发了处理和数学理解它们生成的证明的技术。我们设计和分析了许多逻辑的证明系统，而深度推理方法是目前证明理论中最普遍的方法之一，适用于广泛的逻辑。有明确的证据表明，深度推理将进一步扩大其范围，扩展到抵制传统证明论方法的逻辑。这是一个非常令人满意的情况，为新的探索奠定了坚实的基础。总之，在这次研究中，我们基本上是想提高我们寻找形式证明的能力。在寻找给定陈述的证明时，有两个成本组成部分：1)我们正在寻找的证明的大小，以及2)找到它所需的工作量。方面1通常被称为证明的“复杂性”，而方面2与一种被称为“非决定论”的性质有关：复杂性和非决定论越低，就越容易找到证据。不幸的是，这两个方面并不是独立的，通常只能以牺牲其中一个为代价来改进。深度推理有可能在两个成本组成部分上都做得更好，同时也有可能比旧方法做得更好。这是因为它在设计推理规则和演绎系统时给予了我们极大的灵活性，基本上，我们可以用来构建和找到证据的算法。我们提出的项目将利用这种灵活性和我们过去在证明理论中使用的成功技术的知识，以创建新的、高效的演绎系统。通过开展这项研究，1)我们将通过解决一些关于形式证明大小的基本问题，将对深度推理的兴趣扩展到证明复杂性领域，2)我们将为高效形式证明在计算机系统中的直接应用奠定坚实的基础。我们希望我们的计划能够促进在证明理论和证明复杂性方面的进一步研究。我们的研究的直接好处将是证明理论和证明复杂性这两个研究界。从更长远的角度来看，我们的研究将通过提供设计可靠和安全的计算机系统的方法来造福社会。

Proof theory and proof complexity study formal proofs both in mathematics and in theoretical computer science. Resorting to formal proofs is our best chance of not making mistakes. Formal proofs are relatively simple and clear objects, which can be verified both by humans and computers with extremely high confidence. Proofs can be studied for different languages, or logics, corresponding to different domains of discourse and applications.Computers are playing a major role in our lives: our safety, and the safety of our goods, depends on their reliable and secure behaviour. We all know that the security of computer systems is constantly challenged, and some of our best hopes for maintaining computer systems under control is to develop computer languages and verification tools based on formal proofs. This contributes to a shift of interest in formal proofs from mathematics to theoretical computer science. More than mathematics, computer science is concerned with quantitative issues like the efficiency by which we can prove theorems. For example, the famous problem P vs NP is directly connected with theorem proving, and belongs to both proof theory and proof complexity.Six years ago, the PI of this proposal, together with the RA for which funding is requested, and together with his students and colleagues, launched a research initiative about a new methodology in proof theory, called `deep inference'. Deep inference looks at formal proofs in a way that is much closer to computer science than was the case before, because it exploits their information content in a way which is, in principle, more efficient than with traditional methods. To establish deep inference as a proper area in the field of proof theory, we designed proof systems and developed techniques for manipulating and mathematically understanding the proofs they generate. We designed and analysed proof systems for many logics, and deep-inference methods are now some of the most universal in proof theory, being applicable to a vast range of logics. There is clear evidence that deep inference is going to expand even further its range, to logics that resisted traditional proof-theoretic methods. This is a very satisfying situation, and it constitutes a solid foundation for new explorations.In a few words, in this research, we basically want to improve on our ability of finding formal proofs. There are two cost components in the search for a proof of a given statement: 1) the size of the proof we are looking for, and 2) the amount of work necessary to find it. Aspect 1 is usually called the `complexity' of the proof, and aspect 2 has to do with a property called `non-determinism': the lower the complexity and the non-determinism, the easier it is to find proofs. Unfortunately, the two aspects are not independent, and usually one can only be improved at the expense of the other.Deep inference has the potential of doing better than the old methods on both cost components and at the same time. This is due to the extreme flexibility it gives us in designing inference rules and deductive systems, which are, basically, the algorithms by which we can build and find proofs. The project we propose will use this flexibility and our knowledge of successful techniques used in proof theory in the past, in order to create new, efficient deductive systems.By carrying out this research, 1) we will extend to the area of proof complexity the interest in deep inference, by addressing some fundamental issues about the size of formal proofs, and 2) we will establish firm grounds for direct applications of efficient formal proofs in computer systems. We expect our programme to stimulate further research both in proof theory and proof complexity.The immediate benefits of our research will be to the two research communities of proof theory and proof complexity. More in perspective, our research will benefit society by providing ways of designing reliable and secure computer systems.