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. More recently, Connect++ has also become a basis for the implementation of proof certification standards.

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

You can download the source from:

https://www.cl.cam.ac.uk/~sbh11/connect++.html

The version currently available is V0.7.0.

The Connect++ theorem prover is now part of the Thousands of Problems for Theorem Provers (TPTP) infrastructure. You can use it here:

https://tptp.org/cgi-bin/SystemOnTPTP

Contact

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

Home page: https://www.cl.cam.ac.uk/~sbh11.

How to build and use Connect++

Note to M$ Windows users. Sorry, but so far the distribution is very much designed for Linux/OS X. I intend at some point to extend the cmake infrastructure to build for Windows, but don't expect this to happen any time soon. Go on! Install Linux! (You know you want to...)

Having said that, you may of course find that cmake can generate a project file for Visual Studio or similar. I haven't tried this. If you try it, please let me know how you get on. (One person has now provided feedback that they've compiled Connect++ under Windows with a small number of modifications - many thanks!)

Install the Boost C++ libraries

Connect++ uses Boost libraries for parsing, for processing command-line options, and for computing hash functions. Also, for some random number generation. Depending on what's being developed there may be other uses involved. Mostly the Boost libraries are header-only, but command-line processing (at least) requires a compiled library.

Your preferred Linux flavour's package manager, along with Homebrew and MacPorts on OS X, will probably make it easy to install the Boost libraries. Alternatively, you can download the Boost libraries from:

https://www.boost.org/

and compile from source.

Connect++ currently uses Version 1_84_0. Install so that the libraries that require compilation are included.

Install SWI Prolog (optional)

Earlier versions of Connect++ used a short Prolog program to verify proofs. This function is now built-in, but the Prolog proof verifier is included in the distribution. If you want to use it, you need SWI Prolog, which is available here:

https://www.swi-prolog.org/

or will probably be provided by the various package managers.

Compile Connect++

If you don't have cmake, install it, either via a package manager or from:

https://cmake.org/

If you have installed the Boost libraries and SWI Prolog in the usual locations then cmake should find and use them automatically:

tar -xf connect++-source-v0.7.0.tar.gz

cd connect++-source-v0.7.0

mkdir build

cd build

cmake ../source

cmake --build .

You should now have the connect++ executable in the build directory.

If cmake can not find the Boost libraries try:

cmake ../source -D BOOST_INCLUDEDIR=/where/is/include -D BOOST_LIBRARYDIR=/where/is/lib

If you don't need the Prolog proof verifier use:

cmake ../source -D INCLUDE_PROLOG=OFF

If you do want the Prolog proof verifier, but cmake can't find the swipl executable, use:

cmake ../source -D swipl_PATH=/where/is/swipl

When make succeeds, try:

./connect++ --version

./connect++ --help

and you should see some useful information.

Run Doxygen

The source is commented in a format allowing Doxygen to generate documentation. The output can be found on the project web site:

https://www.cl.cam.ac.uk/~sbh11/connect++.html

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

https://www.doxygen.nl/

Prove a theorem

Connect++ reads problems in the CNF and FOF formats defined by the Thousands of Problems for Theorem Provers (TPTP) collection. It will process include, and if it detects the use of equality it will generate the necessary axioms (unless you ask it not to). TPTP along with various tools and a description of the format can be found here:

https://tptp.org/

If you have TPTP installed then you can set the environment variable TPTP to the relevant path and Connect++ will use it:

export TPTP=where/to/find/TPTP-v9.2.1

Alternatively use the --tptp command-line argument. Assuming you've set the TPTP environment variable and have TPTP installed, you should now be able to do, for example:

./connect++ --schedule default --timeout 10 Problems/SET/SET002+3.p

The last line of the output should be:

% SZS status Theorem for SET002+3

Note that by default Connect++ implements the TPTP standard of treating constants in double quotes as distinct objects. So for example:

fof(distinct_objects, conjecture, "Sean" != "Tarquin").

will be a theorem, but:

fof(distinct_objects, conjecture, Sean != Tarquin).

won't. If you don't want this behaviour use the --no-distinct-objects command-line option.

Other environment variables

The CONNECTPP_PATH environment variable can be used to set the destination for Prolog-readable representations of the proof and the matrix. These will be produced if you use the --prolog command-line option.

Visualising proofs

Connect++ can produce a LaTeX-formatted visualisation of a proof. Use the --latex command-line option to do this:

./connect++ --schedule default --timeout 10 --latex default Problems/SET/SET002+3.p

Using --latex default will produce a file ./latex_proof.tex. When processed you may find you have to zoom in on it as proofs can be quite large. If you want a different filename/location then specify it instead of default.

If you take a look at:

./connect++ --help

you will also find options for producing LaTeX output in the format of a proof tableau, and a similar option for producing Graphviz output. Unsurprisingly, you'll need to install Graphviz:

https://graphviz.org/

For example:

./connect++ --schedule default --timeout 10 --graphviz-tableau default Problems/SET/SET002+3.p

dot -Tpdf graphviz_tableau_proof.dot > tableau.pdf

will provide a tableau visualisation of the proof.

Verifying proofs (the quick and dirty way)

Connect++ can output a (simple) proof certificate and verify it. You can do this manually, or ask for it to happen automatically. Manual verification requires SWI Prolog, as mentioned above.

Why "quick and dirty"? Well, this procedure makes two shortcuts. First, it does not verify any clause conversion that takes place. Second, it only checks that each step of the connection calculus has been applied correctly to construct a proof. Since V0.7.0 Connect++ has been able to produce a stronger proof certificate. Keep reading if that's what you need.

Manual verification

Run for example:

./connect++ --schedule default --timeout 10 --prolog Problems/SET/SET002+3.p

Connect++ places the files matrix.pl and proof.pl in CONNECTPP_PATH. These are prolog-readable summaries of the matrix and proof.

In the build directory you will find check_proof. (Assuming you included it in the build.) Now place matrix.pl and proof.pl in the same directory as check_proof and run:

./check_proof

for a (very) short summary output or:

./check_proof v

For a detailed output.

Automatic verification

To get automatic verification when a result is proved, use the --verify command-line argument:

./connect++ --schedule default --timeout 10 --verify Problems/SET/SET002+3.p

The last line of the output from the prover should now be:

% SZS status Theorem for SET002+3 : Verified

If you see FailedVerification instead of Verified then something is wrong!

If you want a detailed explanation use --full-verify.

Verifying proofs using the TPTP standard output format

If you run:

./connect++ --schedule default --timeout 10 --tptp-proof default Problems/SET/SET002+3.p

you will receive a detailed proof in the TPTP format. See

https://tptp.org/UserDocs/QuickGuide/Derivations.html

https://tptp.org/Proposals/TableauxFormatProofs/index.shtml

for details.

This format supports a much more involved procedure for verifying derivations. (In fact, the process is one that's probably much more involved than you expect!) Simply put, every step in the proof is independently verified by a separate automated theorem prover. (And a lot of other stuff happens as well!) This includes each individual step in any clause conversion. For example, if you Skolemize then ideally you need to prove that the formulas before and after that step are equisatisfiable. The TPTP approach does precisely this.

TPTP has a checker for properly formatted derivations, called GDV:

https://tptp.org/Seminars/GDV/Summary.html

This should give you an idea of the complexities involved. There is also a tool called IDV for interactively exploring derivations.

Release Notes

The actual proof process has not changed much (if at all) since the last version. This version primarily exists to implement the new TPTP proposal for the output of derivations for clausal connection tableau proofs.

You can find many, many details here:

https://tptp.org/Proposals/TableauxFormatProofs/index.shtml

https://cca.informatik.uni-freiburg.de/weidenbach60/SutcliffeHoldenBaksys-TPTP-Clausal-Tableaux-Proofs.pdf

https://www.youtube.com/watch?v=YhzIvF1M9qo

A word of warning! Definitional clause conversion is common in connection provers. Connect++ will output a derivation certifying definitional conversion, if its proof requires it. However the development of both Connect++ and the GDV verifier are ongoing works in progress and at the time of release you will probably find that derivations including definitional clause conversion do not play nicely with GDV. If you really want to verify a proof, try running without the default schedule and using --no-definitional to force standard clause conversion.

Other additions in this release:

LaTeX output of proofs in tableau format.
Graphviz output of proofs in tableau format.

TODO

A related project described here:

https://arxiv.org/abs/2507.11349

has similar aims to the TPTP approach to verifying derivations. I aim to implement the SC-TPTP format in a future release.

Other planned additions.

Further work is needed to make definitional clause conversion in derivations work in conjunction with the GDV verifier.
At present the parser does not read annotations after formulas. For example, SYN000-2.p will not currently parse correctly.
The TPTP $distinct predicate is not currently implemented.
Allow further flexibility by possibly exploring right branches first.
It is hoped that Version 0.8.0 should have significant further improvements in terms of speed.

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 First International Workshop on Automated Reasoning with Connection Calculi (AReCCa), CEUR Workshop Proceedings, Volume 3613, pages 95--106, Prague, Czech Republic, 18th September 2023.

https://ceur-ws.org/Vol-3613/