Joshua Blinkhorn

Profile

Before joining the University of Leeds as a PhD student in 2016, I studied mathematics with the Open University.

As an undergraduate I found most interest in the subject of mathematical logic.

Research interests

Groundbreaking work of Kurt Gödel published in 1931 dealt a powerful blow to Hilbert's Programme. Hilbert sought a complete axiomatisation of mathematics that was provably free from contradiction; the Incompleteness Theorems demonstrate, in effect, that this is impossible - at least in the sense Hilbert intended. Any arithmetic formalism capable of describing basic arithmetic is essentially incomplete; moreover, it is unable to prove its own consistency.

A more modern approach towards Hilbert's original goals encompasses other advances witnessed later in the twentieth century; in computer science, algorithms and computational complexity. A corollary of the Incompleteness Theorems states, loosely, that there is no algorithm for deciding the truth of arbitrary mathematical statements. That given, it is natural to seek areas of knowledge that are algorithmically accessible to us in practice. Automated Theorem Proving (ATP) is a field that has seen significant practical progress. Research in SAT solving, the subfield that automates search and decision procedures for propositional logic, has been enormously successful, with solvers routinely solving instances in millions of variables, despite the NP-hardness of the underlying decision problem.

My research interests are in the field of proof complexity, currently the main driver for understanding the power and limitations of automated solvers. The relationship consists in the notion that the trace of a solver on an unsatisfiable instance can be interpreted as a proof of falsity in the corresponding proof system.

I work mainly with the proof complexity of quantified Boolean formulas (QBF), where propositional logic is supplied with quantification over truth values, at the expense of PSPACE-completeness above the NP-completeness of SAT. By understanding the simulation structure of QBF proof systems, we hope to understand better the relative strengths of current QBF solving techniques. This entails working with lower bounds; finding families of false formulas that require exponential-size proofs in the one system, but admit short proofs in the other. One strong goal is to develop general techniques for proving such lower bounds. Some techniques (such as feasible interpolation) may be lifted to QBF from propostional proof complexity but others (such as size-width relations) may not.

The recent introduction of dependency schemes in QBF solving is a technique that emphasizes the inherent difference between SAT and QBF. Roughly speaking, the idea is to translate the linear order of the quantifier prefix into a partial order, describing more accurately the semantic dependencies of the instance. As such, dependency schemes are closely related to dependency quantified Boolean formulas (DQBF), a superset of QBF whose decision problem is NEXP-complete. I am interested in the unexplored relationship between these two fields, and the relative complexities of QBF proof systems parametrised by dependency schemes.

Qualifications

  • BSc (Honours) Mathematics, Open University

Publications:

Loading...