Complexity and Non-determinism in Deep Inference

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.