Connect++ is a fast, readable, C++ implementation of a connection prover for first-order logic. It is designed somewhat in the spirit of MiniSAT, with the aim of providing a reference implementation that is easily modifiable by others. In particular, it aims to provide a basis for experiments on improving automated theorem provers using machine learning.

Connect++ is licensed under GNU General Public License (GPL) Version 3.

You can download the source here:

https://www.cl.cam.ac.uk/~sbh11/connect++/connect++-source-v0.1.tar.gz

The version currently available is V0.1, and is the first public release.

Contact

Sean Holden is the author of Connect++ and can be contacted at sbh11@cl.cam.ac.uk.

How to build Connect++

1. Install the Boost C++ libraries

   Connect++ uses Boost libraries for parsing, for processing command line options, and for computing hash functions. (Depending on the current state of development there may be other uses involved.)

   Mostly the Boost libraries are header only, but command line processing at least requires a compiled library.

   I believe MacPorts or similar may allow one-command installation, but I recommend installing from source as I've had a much better experience when I can control exactly where the header files and libraries are located.

   You can download the Boost libraries from:

   https://www.boost.org/

   Connect++ currently uses Version 1_83_0. (Or in some circumstances 1_79_0, and both work fine.) Follow the instructions to install the version with the libraries that require compilation included.

   Finally, you will need to edit the Makefile to reflect wherever it is you have installed the Boost libraries.

2. Compile Connect++

   If you've got the paths to the Boost libraries correct in the Makefile, then a simple "make" should give you the "connect++" executable. Try:

   ./connect++ --version

   ./connect++ --help

   and you should see some useful information.

3. Run Doxygen

   The source is commented in a format allowing Doxygen to generate documentation. The current output is linked to on the left of this page.

   If you want to reformat it to your taste then you can install Doxygen from:

   https://www.doxygen.nl/

4. Prove a theorem

   Familiarise yourself with the Thousands of Problems for Theorem Provers (TPTP) format for first-order problems in CNF form.

   https://tptp.org/

   The basic command you need is:

   ./connect++ --schedule default foo.tptp

   but there are many command line options available. Again, see:

   ./connect++ --help

   Some more comprehensive guidance on command line options and scheduling is a work in progress and will appear here shortly.

   Happy proving!

5. Citation

   If you find Connect++ useful, please cite it by way of the following publication, which describes the motivation and general thinking behind it:

   Sean B Holden. CONNECT++: A New Automated Theorem Prover Based on the Connection Calculus. In Proceedings of the International Workshop on Automated Reasoning with Connection Calculi (AReCCa), Prague, Czech Republic, 18th September 2023.

Things to note

(To be completed for Version 0.2.)

1. You will find in the source the class FOF, which represents first-order logic in full. You will also find that the TPTPParser will parse first-order logic from TPTP files. However Connect++ at present supports only clause form. First-order logic is a work in progress and will be completed for Version 0.2. The incomplete infrastructure is in the source because removing it (particularly from the TPTPParser) would just be counterproductive.

2. The TPTPParser does not presently deal with includes.

3. In order to support the generation of proofs as training data, some work has been done to allow generation of multiple proofs. This is not yet fully implemented.