of Computer Science
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
Address (College)Trinity College
Phone+44 (0)1223 763725 (University)
+44 (0)1223 338452 (College)
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++ is currently a work in progress but my aim is to open-source it in 2023. Here's a bit of a teaser...
Step 1: present your problem in TPTP format
You can find the specification for the TPTP format here.
Step 2: define a scheduleYou 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:
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:
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...
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.
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!
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.