Research Interests
I'm interested in automated reasoning, i.e. getting computers to "think" logically.
This has plenty of applications (including mathematics and software verification), but personally I just think it's neat.
You might call this "symbolic" or "good old-fashioned" AI — in contrast to what the press calls "AI" at the minute.
Vampire
I help maintain Vampire, a world-class fully-automatic theorem prover.
Read our CAV 2025 survey!
Vampire is a big beast, applying lots of different strategies to prove many different theorems.
You can think of it as a machine for deducing consequences very efficiently.
Vampire is my go-to testbed for trying new ideas and the code is much easier to navigate than it used to be.
Machine Learning and Automated Reasoning
Traditional computer reasoning systems do not learn from their experience as we do.
Why not?
I wrote my PhD thesis on this topic — it turns out to be harder than I'd hoped!
I've done some work on representing logical data for consumption by neural networks and guiding theorem provers in various more-or-less straightforward ways.
This all worked for me to some extent, but what I was missing was scale and persistence: a large team centred around Prague were able to make enormous progress this way.
Recently I've been having a re-think about how to achieve the kind of free lunch I'm looking for by changing the rules of the game.
Applications
It's fun to try to apply automated reasoning in new areas, especially where it looks unlikely at first.
I've been involved with efforts in security and game theory, for example.
Automated reasoning's biggest customer is still interactive theorem proving, which is a very natural pairing: automated reasoning fills in the easy parts as users write large computer-checked proofs.
Unfortunately systems like Lean use complex dependent type theories as their foundation, which are very hard to automate.
I'd like to see the ITP community return to simpler times and simpler foundations: the HOL family, Mizar and Metamath are all great.
Knuckledragger, Naproche, LISA and Natty are more recent innovations.
Proof Checking and Transformation
Once you have a proof from an automated system, it might be nice to check it or transform it into a different kind of proof (watch this space).
This is somehow not yet a solved problem!
There are both technical problems (how do we do handle e.g. Skolemnisation?) and engineering considerations (who wants to deal with Vampire's hundred-odd existing inferences?).
Connection Calculi
Systems like Vampire reason "forwards" from the input and the negated goal, towards a proof by refutation.
What if you instead reason "backwards" from the goal towards axioms?
Connection methods embrace this idea and produce very concise implementations, like leanCoP.
I've been trying to bring modern automated reasoning techniques like SAT solving, constraint learning, and specialised handling of equality to connection systems.
I am very grateful to the connection community for being so welcoming!
Automated Reasoning Oddities
I'm usually playing with some strange underhand tricks for automated reasoning, much of it unfinished.
My current favourite toys are algebraic logic, magic sets, and symmetry breaking.
I'd also love to apply something rogue like a Fourier transform from wider mathematics to automated reasoning, just to freshen things up a bit.
Write me if you have a wonky idea in this area!
TPTP
I am slowly starting to help Geoff Sutcliffe with the TPTP World, which is "established infrastructure used by the Automated Theorem Proving (ATP) community".
At some point TPTP stood for "Thousands of Problems for Theorem Provers" - the benchmark set is one part of the wider World.
