QBF Proofs and Certificates

Imagine a mathematical theorem, many people would be familiar with simple work like The Sum of Angles of a Triangle or more famous theorems like Fermat`s Last Theorem. Mathematicians are valued not only for their insights for coming up with these theorems, but finding proofs that confirm that these theorems will remain true no matter how many advances are made in mathematics. Theorems which have proofs, will remain uncontradicted for the rest of eternity. While proofs were an important part of the study of classically mathematical objects, such as numbers, functions and equations. It took until the 20th century for proofs to be taken seriously as mathematical objects themselves, with the work of the Austrian logician Godel and many others. In modern times, proofs are not only studied as an intricate part of mathematical proof theory as well as the philosophy of logic, but unmistakeably part of modern computing. Proofs are part of payment authentication, hardware verification and security. With computing in mind, we are best understanding proofs in its most natural form as a certificate of logical truths (1s) and falsities (0s), certifying the solutions to computing problems that also work in binary. Most of the time we want proofs to be as small as possible, so that uploading our proofs to a third party has a minimal effect on the time it takes to complete a task. We ask the fundamental question in our line of research: how small can we make our proofs? Size, here is measured in the number of binary b its we need to express our proofs. And we understand the size of a proof may depends on a theorem, as the size of a theorem gets bigger we can reasonably expect the size of a proof to grow bigger, but how much bigger? If a proof size grows exponentially in the size of a theorem, we would have no hope to deal with practical applications. Hence the field of Proof Complexity is made to study these. Our research looks at a particular type of logic: Quantified Boolean Formulas (QBF), specifically developed to reformulate difficult problems in computer science as logic problems. Our aim is to go into finer detail on how to make proofs shorter for a wide array of applications. In particular we take inspiration from advances made in the practical task of solving QBFs and hope we can design a robust way of verifying their solutions. Our work sits in-between the practical science of solving and the theoretical science of proof theory. Beyond the verification aims of our work, we also hope to have an impact and inspira tion on this wider practice and theory.

This project made theoretical advances that allows computer generated proofs to be smaller and easier to check- strengthening the foundations of secure and trustworthy digital technologies. Many modern digital systems are highly complex but perform critical tasks such as user authentication, financial transactions and safety controls. This means these systems need to be extremely reliable. Thus many already use hidden mathematical proofs to ensure correctness of the operations, and highly tested and theoretically robust independent software is used to check these proofs automatically. Over time many different proof techniques have been developed, either in hopes of improving an existing approach or to tackle new kinds of problems. Proofs can only work as long as they can be checked reliably, and a large number of rules makes automatic proof checking harder and more prone to errors, which can be catastrophic. Our approach started by grouping together a number of similar problems, and then our main contribution is the simplification of a large number of proof rules across these problems into just five simple rules. This was eventually presented in the paper Better Extension Variables in DQBF via Independence as the proof system, which we have called Ind Ext QU-Res, acts as a culmination of our work. The search for such a proof system has been identified as long-term goal before the project began, and its realisation stands as a significant theoretical contribution. Most of the other papers supported by the project during the three years, either build essential groundwork for this proof system, contribute in some way to proving the eventual properties of this proof system, or show that other proposed combinations of rules have critical weaknesses. The most common weakness is that a proof system has a handful of cases where proofs unavoidably grow to enormous unwieldy sizes and are practically impossible to store and even harder to check. The other contribution is starting the work that involves numerical data, rather that pure binary data (True/False). This has led to new advances in both solving techniques, the certification of solving techniques and computational theory. This broadens the potential of our work. While there is still some work left to close the gap between theory and practice, and broaden the scope of both into new kinds of problem, overall the project has strengthened the foundation of computer automated verification by making new proof systems that are simpler but more powerful.