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.2.1.tar.gz

The version currently available is V0.2.1.

Contact

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

How to build and use 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_84_0. 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

   Connect++ reads problems in the CNF and FOF formats defined by the Thousands of Problems for Theorem Provers (TPTP) collection. It will process "includes", 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-v8.2.0

   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 Problems/SET/SET002+3.p

   The last line of the output should be:

   % SZS status Theorem for SET002+3

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

   Happy proving!

5. Other environment variables

   If you run Connect++ from the directory that the tar file extracts to, then all should be well.

   If you want to run the executable from elsewhere you may need to set the CONNECTPP_PATH environment variable. This should be set to the path for the directory containing the Connect++ prolog directory. Alternatively, use the --path option.

   This is mainly important if you want automatic proof verification (Section 7 below).

6. Visualising proofs

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

   ./connect++ --schedule default --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.

7. Verifying proofs

   Connect++ can output a proof certificate and verify it. You can do this manually, or ask for it to happen automatically. The program used to verify proofs requires SWI Prolog, which can be obtained here:

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

   Manual verification

   Run for example:

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

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

   In the same directory you will find check_proof. If necessary edit the first line of check_proof to specify the directory for the SWI Prolog executable swipl.

   Now run:

   ./check_proof

   for a (very) short summary output or:

   ./check_proof v

   For a detailed output.

   Automatic verification

   Set the CONNECTPP_SWI_PATH environment variable to the path for the SWI Prolog executable swipl. Now use the --verify command-line argument:

   ./connect++ --schedule default --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! Note that Connect++ needs the prolog/tmp directory in order to do this.

8. Release Notes

   Quite a lot has happened since Version V0.1:

   • The data structure for Terms now does proper hash consing. As a result this implementation is considerably faster.

   • V0.1 did not process TPTP include and only handled CNF format problems. V0.2 processes <>include"s and also handles FOF format problems. Use --show-clauses if you want to see a clause conversion of an FOF problem.

   • Outputs for the prover now implement the SZS ontology:

     https://www.tptp.org/Seminars/SZSOntologies/Contents.html

   • For the time being (and I suspect unless there is a definite demand) there is no longer the option to use DNF/positive representation.

   • Verification of proofs can be done automatically.

   • Important paths can be read from environment variables or specified at the command line.

   Changes from V0.2 to V0.2.1 are quite minimal. Production of an output summary is now optional. The resources directory is no longer needed. You can specify a destination for LaTeX output.

9. Issues

   At present the parser does not read annotations after formulas. For example, SYN000-2.p will not currently parse correctly.

10. 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/

11. Coming soon in Version 0.3...

    • Definitional clause form conversion.

    • Extended scheduling support.

    • At least one new heuristic.

    • Simpler installation.

    • And lots more goodies...