Repository logo
 

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

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Abstract

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.

Description

Keywords

Journal Title

CEUR Workshop Proceedings

Conference Name

International Workshop on Automated Reasoning with Connection Calculi (AReCCA)

Journal ISSN

1613-0073

Volume Title

Publisher

Publisher DOI

Publisher URL


Version History

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