Email

Please use the @cl form of address in preference to any other you may have. (Executive summary: the University decided to farm out its email provision to Micro$oft, with disasterous consequences. By using the correct email address your message should be handled by a proper, standards-compliant alternative, and therefore stands a much better chance of reaching me.)

Address (University)

University of Cambridge
Department of Computer Science and Technology
The Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge
CB3 0FD

Address (College)

Trinity College
Cambridge
CB2 1TQ

Phone

+44 (0)1223 763725 (University)
+44 (0)1223 338452 (College)

Orcid

0000-0001-7979-1148

Also available...

...on DBLP and Semantic Scholar.

If you want to study with me, please read the FAQs before doing anything else.

Lean theorem provers are great: who doesn't want something implemented in a few lines of Prolog? However, they have some definite problems:

The automated theorem-proving (ATP) world likes to see things going faster and/or more things being proved. If your prover is implemented in Prolog it starts at a disadvantage.
Many of the best heuristics involve getting control over the backtracking process, and this is not necessarily straightforward if you want something better than cut.
There are lots of other ways you might incorporate good heuristics into the proof search, but influencing a Prolog-based search in the way you want to may not be straightforward.
If you want to use machine learning, then getting Prolog, Python and C++ to play nicely together on a high-performance computing facility can be, for want of a better word, frustrating.

Connect++ is a connection prover implemented in C++ specifically with the aim of making it fast, and easy to incorporate new heuristics and machine learning methods.

Connect++ was open-sourced in 2023, and is a work in progress. Here's a quick introduction...

Step 1: present your problem in TPTP format

% % Problem from "Guiding Inference in Connection Tableaux % by Recurrent Neural Networks", Piotrowski and Urban, % CICM 2020. % cnf(c1, unknown, p(X)). cnf(c2, unknown, r(X,Y) | ~p(X) | q(Y) ). cnf(c3, unknown, s(X) | ~q(b) ). cnf(c4, unknown, ~s(X) | ~q(X) ). cnf(c5, unknown, ~q(X) | ~r(a,X) ). cnf(c6, unknown, ~r(a,X) | q(X) ).

You can find the specification for the TPTP format here. Connect++ reads problems in both CNF and first-order format.

Step 2: define a schedule

You can run Connect++ using a large number of options for parameters related to start clause selection, restriction of backtracking and so on.

The use of --schedule default on the command line directs Connect++ to use a straightforward schedule rather than fixed parameters. At present the default schedule looks like this:

sbh11@sbh11 resources % more default_schedule.txt 2 --pos-neg-start --complete 7 ; 60 --conjecture-start ; 20 --pos-neg-start --restrict-start ; 2 --conjecture-start --reorder 23 ; 2 --pos-neg-start --restrict-start --reorder 29 ; 2 --conjecture-start --reorder 37 ; 2 --pos-neg-start --restrict-start --reorder 41 ; 2 --conjecture-start --reorder 47 ; 0 --pos-neg-start --all-backtrack ; sbh11@sbh11 resources %

But you can specify a file containing your own schedule and Connect++ will parse it.

Step 3: run the prover

Unsurprisingly, it doesn't have too much trouble with the example quoted above:

Step 4: take a look at the proof

The use of --latex on the command line directs Connect++ to produce a LaTeX representation of the first proof it finds.

Proofs tend to be wide, so this illustration is cropped. The full diagram is here.

Step 5: verify the proof's certificate

The use of --prolog on the command line directs Connect++ to produce a certificate for the first proof it finds.

This can be checked by a short Prolog program:

Start Clause: [-s(_13892),-q(_13892)] ---------- Left extension: depth = 2 C2 = [s(_13976),-q(b)] L2 = s(_13976) Unification OK. C = [-q(b)] P = [-s(_13892)] L = [] ---------- Left extension: depth = 3 C2 = [-r(a,_18196),q(_18196)] L2 = q(_18196) Unification OK. C = [-r(a,b)] P = [-q(b),-s(_13892)] L = [] ---------- Left extension: depth = 4 C2 = [r(_18406,_18408),-p(_18406),q(_18408)] L2 = r(_18406,_18408) Unification OK. C = [q(b),-p(a)] P = [-r(a,b),-q(b),-s(_13892)] L = [] ---------- Reduction: Lit resolved in path: -q(b) Unification OK. C = [-p(a)] P = [-r(a,b),-q(b),-s(_13892)] L = [q(b)] ---------- Left extension: depth = 6 C2 = [p(_19182)] L2 = p(_19182) Unification OK. C = [] P = [-p(a),-r(a,b),-q(b),-s(_13892)] L = [q(b)] ---------- Axiom ---------- Right extension: depth = 6 C = [] P = [-r(a,b),-q(b),-s(_13892)] L = [-p(a),q(b)] ---------- Axiom ---------- Right extension: depth = 4 C = [] P = [-q(b),-s(_13892)] L = [-r(a,b)] ---------- Axiom ---------- Right extension: depth = 3 C = [] P = [-s(_13892)] L = [-q(b)] ---------- Axiom ---------- Right extension: depth = 2 C = [-q(_13892)] P = [] L = [-s(_13892)] ---------- Left extension: depth = 3 C2 = [-r(a,_19704),q(_19704)] L2 = q(_19704) Unification OK. C = [-r(a,_13892)] P = [-q(_13892)] L = [-s(_13892)] ---------- Left extension: depth = 4 C2 = [r(_19914,_19916),-p(_19914),q(_19916)] L2 = r(_19914,_19916) Unification OK. C = [q(_13892),-p(a)] P = [-r(a,_13892),-q(_13892)] L = [-s(_13892)] ---------- Reduction: Lit resolved in path: -q(_13892) Unification OK. C = [-p(a)] P = [-r(a,_13892),-q(_13892)] L = [q(_13892),-s(_13892)] ---------- Left extension: depth = 6 C2 = [p(_20232)] L2 = p(_20232) Unification OK. C = [] P = [-p(a),-r(a,_13892),-q(_13892)] L = [q(_13892),-s(_13892)] ---------- Axiom ---------- Right extension: depth = 6 C = [] P = [-r(a,_13892),-q(_13892)] L = [-p(a),q(_13892),-s(_13892)] ---------- Axiom ---------- Right extension: depth = 4 C = [] P = [-q(_13892)] L = [-r(a,_13892),-s(_13892)] ---------- Axiom ---------- Right extension: depth = 3 C = [] P = [] L = [-q(_13892),-s(_13892)] ---------- Axiom ---------- true .

Step 6: improve the process by adding some machine learning

This is the reason I wrote Connect++ in the first place! There is of course existing literature addressing this, but there's also plenty of room for new things.

Step 7: profit...

Still working on this part...

Latest news:

July 2024: The Connect++ theorem prover has won Best Newcomer at the CADE ATP System Competition (CASC) - the World Championship for automated theorem proving systems.
27th March 2024: The Connect++ theorem prover is now part of the Thousands of Problems for Theorem Provers infrastructure. You can use it here: https://tptp.org/cgi-bin/SystemOnTPTP.
New publication: MUGI-MRI: Enhancing breast cancer classification through multiplex graph neural networks in DCE-MRI, Francesco Ceccarelli, Salvatore Vitabile, Francesco Prinzi, Sean B. Holden, and Pietro Liò. Proceedings of the International Joint Conference on Neural Networks (IJCNN), 2024. Accepted for publication.
New publication: Integrating structure and sequence: Protein graph embeddings via GNNs and LLMs, Francesco Ceccarelli, Lorenzo Giusti, Sean B. Holden, and Pietro Liò. Proceedings of the 13th International Conference on Pattern Recognition Applications and Methods (ICPRAM), 2024.
New publication: Connect++: A new automated theorem prover based on the connection calculus, Sean B Holden. Proceedings of the International Workshop on Automated Reasoning with Connection Calculi (AReCCA), 2023.
New publication: A syntax for connection proofs, Jens Otten and Sean B Holden. Proceedings of the International Workshop on Automated Reasoning with Connection Calculi (AReCCA), 2023.
New publication: Markov decision processes for classical, intuitionistic, and modal connection calculi, Fredrik Rømming, Jens Otten and Sean B Holden. Proceedings of the International Workshop on Automated Reasoning with Connection Calculi (AReCCA), 2023.
6-1-23: I am now Associate Editor of the IEEE Transactions on Artificial Intelligence.
6-1-23: Surprised, but intrigued that I now have an entry on IMDb as a result of my TV activities.
Tutorial talk: my 2021 half-day tutorial talk from CADE-28 is now available in the Research section.
New publication: Towards a competitive 3-player Mahjong AI using deep reinforcement learning, Xiangyu Zhao and Sean B. Holden. Proceedings of the IEEE Conference on Games, 2022.
New publication: Bayesian ranking for strategy scheduling in automated theorem provers, Chaitanya Mangla, Sean B. Holden, and Lawrence Paulson. Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR), 2022.
My book Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT has now been published.

Don't delay! Get your copy now! 200 pages of machine learning and theorem proving goodness!
Congratulations to my PhD student Agnieszka Slowick for acceptance of her paper On the Relation Between Distributionally Robust Optimization and Data Curation at AAAI 2022.
My book Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT will be published this year in the Foundations and Trends® in Machine Learning series.