Connect++: A New Automated Theorem Prover Based on the Connection Calculus

Connect++ is an automated theorem prover for first-order logic with equality, based on the clausal connection calculus and designed with three primary goals. The first was to produce a care- fully coded system in a compiled language (C++). The second was to allow the system to support my own research agenda involving the addition of machine learning to connection provers. The third, somewhat inspired by the success of the MiniSAT solver for Boolean satisfiability, was to provide an implementation sufficiently modifiable as to provide a common basis for experiments by others. In addition to these aims I wanted to exploit the opportunities inherent in the connection calculus to explore the production of readable and certified proofs. This paper describes the system as it stands; development is ongoing and some plans for the future are also outlined