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

Conference Object
Change log

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.

Journal Title
Conference Name
International Workshop on Automated Reasoning with Connection Calculi (AReCCA)
Journal ISSN
Volume Title
Publisher DOI
Publisher URL

Version History

Now showing 1 - 2 of 2
2024-01-12 09:51:01
Published version added
2023-12-09 00:31:09
* Selected version