Structure vs. Invariants in Proofs (StrIP)

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science

Abstract

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.

Planned Impact

This fellowship (StrIP) is primarily based in theoretical research, and thus will have principal short-medium term impact on academia and, at a national level, the wider research community. StrIP will advance the state of the art in theoretical computer science, and thus accelerate the general progression of computing industries in the long term.

In particular, StrIP will benefit the software industry, especially in the UK, thanks to the development of techniques that may be applied to Automated Reasoning and programming language theory. More generally, StrIP contributes to the area of Formal Verification, which increasingly affords us the ability to certify the correctness of software in practice. This will have a positive impact on technological innovation in the long term, and thus for the economy too.

In the short term, within the duration of StrIP, I will engage with the wider UK public in the form of outreach events. This may include popular science events, open days or visits to local schools. In particular, I aim to contribute to the public understanding of Formal Verification as a way to build trust in software that we rely on.

Publications

10 25 50

publication icon
Das A (2020) A Functional (Monadic) Second-Order Theory of Infinite Trees in Logical Methods in Computer Science

publication icon
Van Der Giessen I (2023) Admissible rules for six intuitionistic modal logics in Annals of Pure and Applied Logic

publication icon
Gianluca Curzi (2021) Cyclic Implicit Complexity

publication icon
Das A (2020) From QBFs to MALL and Back via Focussing in Journal of Automated Reasoning

publication icon
Gianluca Curzi (2021) Linear Additives

 
Title Linear Inferences 
Description This implementation consists of a tool to check relationships between linear inferences, and to generate them, using characterisations of logic via cographs. 
Type Of Technology Software 
Year Produced 2021 
Impact A paper has been written and submitted, by A Das and A Rice, announcing the software and its outputs. An open problem from previous work by Das and Strassburger was solved as a result. 
URL https://github.com/alexarice/lin_inf
 
Description Popularisation of science talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Public/other audiences
Results and Impact A popular science talk at UoBe Enlightened, a TED-style event taking place at the University of Birmingham.
Year(s) Of Engagement Activity 2020
URL https://www.birmingham.ac.uk/university/building/uobe-enlightened.aspx
 
Description Popularisation talk at St Benedict's School 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact I gave a talk about mathematics and computer science at St Benedict's School in November 2022. It was virtual but was followed by a physical visit.
Year(s) Of Engagement Activity 2022
 
Description School Visit (Kew House School) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact I gave a talk to 50-70 pupils at Kew House school about modern research in theoretical computer science, academic careers, and also university applications.
Year(s) Of Engagement Activity 2020
 
Description School Visit (St Benedicts) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact I instructed two 'guest' lessons to further mathematics students at St Benedict's School in London in December 2022. About a dozen students in each class. I also spoke to several students and teachers during my visit.
Year(s) Of Engagement Activity 2022
 
Description School visit (St Benedicts, virtual) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact 50-60 students attended a popular science talk I gave about the theory of computing. I discussed several aspects of the research area afterwards with the students. I am awaiting feedback from the school about its impact.
Year(s) Of Engagement Activity 2021