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.