=Paper= {{Paper |id=Vol-3613/AReCCa2023_paper7 |storemode=property |title=Connect++: A New Automated Theorem Prover Based on the Connection Calculus |pdfUrl=https://ceur-ws.org/Vol-3613/AReCCa2023_paper7.pdf |volume=Vol-3613 |authors=Sean B. Holden |dblpUrl=https://dblp.org/rec/conf/arecca/Holden23 }} ==Connect++: A New Automated Theorem Prover Based on the Connection Calculus== https://ceur-ws.org/Vol-3613/AReCCa2023_paper7.pdf
                                Connect++: A New Automated Theorem Prover Based
                                on the Connection Calculus
                                Sean B. Holden1
                                1
                                 University of Cambridge, Department of Computer Science and Technology, The Computer Laboratory, William Gates
                                Building, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK.


                                                                         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 carefully 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.

                                                                         Keywords
                                                                         Connection Prover, C++, Machine Learning, Certified Proof, Automated Theorem Prover, System de-
                                                                         scription, First-Order Logic, Clausal Connection Calculus




                                1. Introduction
                                Connect++ is a prover for first-order logic, implemented in C++ and based on clausal connection
                                calculus. The advantages of connection provers, with respect to their goal-oriented search and
                                ability to produce readable proofs, are well-known, and have led to great interest in their use
                                for applying machine learning (ML) to automated theorem proving (ATP). This paper introduces
                                Connect++, and gives a high-level description of the system; it also motivates its development.
                                The paper falls a little outside the usual form of discourse for such papers, combining three
                                related perspectives. First, it is a ‘system description’. Second, it argues for design decisions
                                based on practical experience in conducting large-scale experiments; a pursuit often mandating
                                use of preferred technologies for these two, often disparate research areas. Third, it presents
                                motivations underlying the system’s design decisions, based purely on accommodating the
                                author’s ongoing interest in applying ML in the field of ATP.
                                   Connect++ is open source under the GNU General Public License (GPL) Version 3, and can
                                be downloaded from www.cl.cam.ac.uk/~sbh11/connect++.html. The work in this paper is
                                based on the current development version.
                                AReCCa 2023: Automated Reasoning with Connection Calculi, 18 September 2023, Prague, Czech Republic
                                $ sbh11@cl.cam.ac.uk (S. B. Holden)
                                € https://www.cl.cam.ac.uk/~sbh11 (S. B. Holden)
                                 0000-0001-7979-1148 (S. B. Holden)
                                                                       © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
                                    CEUR
                                    Workshop
                                    Proceedings
                                                  http://ceur-ws.org
                                                  ISSN 1613-0073
                                                                       CEUR Workshop Proceedings (CEUR-WS.org)




                                AReCCa 2023                                                                                               95                                                           CEUR-WS.org




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
   One motivation for Connect++ arose while writing a review of ML applied to satisfiability
(SAT) solvers [1]. It was apparent that there are many SAT solvers, but an enabler of research
over the last two decades was MiniSAT [2], which had a transformative effect. MiniSAT was
fast enough to be competitive,1 while being sufficiently easy to modify that it provided a tool
for other researchers. Much of the research leading to today’s best solvers relied on MiniSAT.
One aim of Connect++ is to provide a similar basis for experiments with connection provers.
(And this is true regardless of any ML.)
   At present, several connection calculus provers are available, implemented in Prolog [5, 6],
C [7], OCaml [8, 9], Rust [10], Python [11] and C++ [12]. This has led to a difficulty which
in the SAT world MiniSAT helped to defray: if two researchers conduct experiments using
different solvers, how do we decouple the effect of any proposed technical contribution from the
characteristics of the solvers? For one to re-implement the other’s work on their own system
would be a solution; but the use of a common solver, in the manner of MiniSAT, would benefit
both sides.
   Further motivation to develop Connect++ arose from two observations made while working
on ML applied to ATP more generally:
    1. The ATP world has two main currencies: proving more things and proving known things
       faster. This motivates the development of ATPs that are inherently fast. It is also in conflict
       with the use of lean ATPs for connection calculus, which tend to rely on languages known
       not to be the fastest.
    2. The ML world is heavily invested in Python, with the most prevalent libraries using
       it to implement their API. To produce research in ML for ATP, one needs to run large
       numbers of experiments. My own groups’ experience in continuing the work presented
       in [13] was that there are significant difficulties in combining Python (for ML), Prolog
       (for leanCoP [5, 6]), and one or more compiled languages supporting the overall process,
       into an experiment on a high-performance computing facility.
These points suggested the development of a connection prover in a fast, compiled language
such as C++, or in Python. C++ emphasizes the speed requirement and is the approach taken
here, addressing Point 1.2 Python is also the subject of current work [11]. Both approaches
address Point 2, but in complementary ways.3
  Further motivations appeared while I worked on the development of Connect++, and these
are some of the most central issues, both discussed further in Section 2:
    1. The lean approach to ATP, exploiting the inherent strengths of Prolog, leads to beautiful,
       compact implementations. However Prolog’s model of computation based on backtracking
       search is not always amenable to the use of ML. (See also Point 2 above.) There are two
1
  I will not be claiming that Connect++ currently competes with the fastest solvers such as E [3] and Vampire [4];
  any comparison is among connection solvers.
2
  While speed was a motivating factor in the choice of language for Connect++, I make no claim in this paper
  regarding its speed in comparison to existing provers—an experimental comparison remains a subject for a future
  paper; here the aim is to provide a general description of the system.
3
  A possible future development that might be of interest would be to incorporate either of these systems into the
  FLoP system [14]. This system employs Python and the C foreign function interface, along with a connection
  prover implemented in OCaml, and hence represents a good target for the kind of simplification envisaged.




                                                       96
                               C ′ , M, {}, {}                     C, M, P, L ∪ {L′ }
                 Axiom                         Start                                    Lemma
   {}, M, P, L                    ǫ, M, ǫ, ǫ                   C ∪ {L}, M, P, L ∪ {L′ }
                           where C ′ is a copy of C ∈ M             where σ(L) = σ(L′ )


  C, M, P ∪ {L′ }, L ∪ {L}                    C ′ \L′ , M, P ∪ {L}, L C, M, P, L ∪ {L}
                               Reduction                                                    Extension
  C ∪ {L}, M, P ∪ {L′ }, L                                   C ∪ {L}, M, P
        where σ(L) = σ(L′ )                             where C ′ is a copy of a clause in M,
                                                            L′ ∈ C ′ and σ(L) = σ(L′ )

Figure 1: Rules for constructing a clausal connection calculus proof. See Figure 3 for an example proof.


      issues here: APIs allowing ML methods to interact with a running Prolog program may
      present a barrier, and Prolog’s model of computation itself can present a limitation.
   2. In particular, the Prolog cut is perfect for leanCop’s backtracking restriction [6]. However
      it is a blunt instrument, and more subtle backtracking heuristics might profitably be
      explored, in turn providing new ways for ML to control the proof search. However the
      implementation of such alternatives in Prolog potentially becomes cumbersome.
While the realisation that the use of C++ supported these points was serendipitous, the overall
design of Connect++ was informed by them as described in Section 4, with the overall aim of
making a system capable of supporting new research.
  A final motivation for Connect++ was to explore the production of readable proofs and
proof certificates.


2. ML for connection calculus: why use C++?
Prolog provides compact implementations for connection provers, but to facilitate ongoing
research on improving connection provers there are good reasons to consider alternatives. In
this section I attempt to explain my reasoning.
   Connect++ implements the clausal connection calculus with lemmata and regularity, as in
Figure 1. The matrix M is the set of clauses for the problem. The path P is a set of literals, as is
the set L of lemmata. A copy of an item has a fresh set of unused variables. An overline denotes
the complement of a literal. Regularity adds the condition

                                  ∀L′ ∈ C ∪ {L} . σ(L′ ) ∈
                                                         / σ(P)

to the Reduction and Extension rules. When applying the Reduction and Extension rules the
substitution is applied to the entire proof. In the case of Regularity and Lemmata we test for
equality using the substitution as it stands, but no further unification is applied.
   The rules in Figure 1 are the basis for a classical backtracking search problem. leanCoP, for
example, arranges this search using Prolog’s underlying search algorithm. It is well-known that
the use of heuristics to order such a search is critical for good performance. For the calculus




                                                  97
described, there is ample scope for learning such heuristics; for example, at any point in the
search there may be multiple ways to extend a partially complete proof, possibly including
multiple applicable uses of Reduction, Extension, or Lemmata rules, and we might aim to
find improved ways of choosing of the next to try. Researchers therefore need to be able to
influence such choices, and the extent to which this is feasible will depend on the details of the
implementation of a prover. This is a particular area where we need a solver implementation
facilitating fine control over search heuristics.
   Some of the most successful heuristics for connection provers go further, relying on the
restriction of backtracking during the proof search [6]. In the Reduction, Extension and Lemmata
rules, L is called the principal literal when the rule is selected as a candidate for extending a
proof. For the Reduction and Lemmata, L is considered solved; for an Extension it is considered
solved if the left sub-tree of the Extension is completed. After L is solved, no other options for
solving it will be considered on backtracking. This heuristic is remarkably effective and the
Prolog cut makes its implementation extremely convenient. However, by moving beyond the
use of cut we potentially open a wide design space of backtracking heuristics. For example,
having solved a literal using Extension, should we backtrack within the left subtree or discard
it completely? (leanCoP, and Connect++ under its default settings do the latter; but use of
the −−explore−left−trees flag forces Connect++ to adopt the former behaviour.) Should
we stop backtracking for a principal literal after it has been solved once, or should we limit
the maximum number of ways we try to solve it? Should we limit backtracking just for this
principal literal, or remove other possibilities once some literal has been solved? There is
considerable opportunity for new work here, and facilitating such research is a key motivation
for Connect++. (See [15] which provides some results in this direction.)
   Other successful heuristics include restriction of backtracking on start clauses, forms of
reordering and randomization [16], and others. Ideally a solver should support all forms of
heuristic, and allow researchers to experiment with them freely. However we should also
consider a further potential need: to modify the operation of the proof search dynamically.
For example, much research on ML for ATP addresses the tuning of heuristics that are then
fixed when attempting new proofs. There is ample evidence from work on SAT solvers that
learning on a per-proof basis is extremely effective. For example, variable selection heuristics are
light-weight learning algorithms adjusting variable choice using feedback obtained while the
proof search progresses. This type of learning also deserves attention in ATP, and the need to
modify heuristics during proof search might be better served by a move away from Prolog.
   A final consideration relates to the way in which the proof search is structured. Some systems
search recursively, trying the left branches of Extensions first. There has been considerable
interest in applying reinforcement learning [17] and Monte-Carlo tree search [18] to connection
provers, and in these cases it makes sense to allow proofs to be constructed in a less constrained
manner. This is the subject of complementary work on representing the process as a Markov
Decision Process [11].




                                                98
         2 --pos-neg-start --complete 7 ;
         60 --conjecture-start ;
         20 --pos-neg-start --restrict-start ;
         2 --conjecture-start --reorder 23 ;
         2 --pos-neg-start --restrict-start --reorder 29 ;
         2 --conjecture-start --reorder 37 ;
         2 --pos-neg-start --restrict-start --reorder 41 ;
         2 --conjecture-start --reorder 47 ;
         0 --pos-neg-start --all-backtrack ;




Figure 2: Default schedule file for Connect++.


3. Connect++
Connect++ supports most of the functionality provided by leanCoP, and has some additional
facilities. It supports restricted backtracking, restriction of start clauses and reordering. It
deals with equality by detecting its use in the input file and adding the necessary axioms; more
sophisticated approaches, such as described in [19, 20], are a subject for future extension. It as-
sumes negative (CNF) representation by default but can use positive (DNF) representation—this
changes the equality axioms added, and the behaviour for some of the start clause selection
options. It supports iterative deepening by path length or tree depth; switching to complete
search after a given depth; and specified start depth and depth increment. It accepts input in
the conjunctive normal form (CNF) format of the Thousands of Problems for Theorem Provers
(TPTP) [21] library. Support for problems in first-order form is a work in progress, and subse-
quently it does not at present support definitional clausal form (DCF) [6]; this is perhaps the
first priority for further development as leanCoP’s standard schedule employs different settings
related to DCF.
   A lesson learned applying ML to SAT is that solvers should avoid hiding within their imple-
mentation, parameters that are potentially important for tuning performance. Instead, such
parameters should be exposed, preferably at the command line, so that they can be adapted to
suit a particular domain of application. Automated systems for this task, such as ParamILS [22],
SMAC [23] and GGA [24] have been used with great success, as has Bayesian optimisation [25].
Connect++ exposes a large, and growing, number of such parameters.
   Some connection provers run with a hard-coded schedule optimized through experiments.
A schedule is a sequence of sets of parameter settings, each element of the sequence being
assigned a percentage of the run time. The prover might start with a schedule line stating that it
should run with full backtracking for 10% of the time, then switch to restricted backtracking for
5% of the time, then switch to a different configuration and so on. Figure 2 shows the current
default schedule used by Connect++, which is similar to that of leanCoP version 2.0. The
differences are necessary as Connect++ does not at present implement definitional clausal
form. This is clearly an effective method, but there is evidence that learning of schedules can be
beneficial [26]. Connect++ supports the use of arbitrary schedules and can read these from
a file in a simple format, making it easy to incorporate the results of ML applied to schedule
choice, and potentially to support the ML process for learning schedules. Referring again to
Figure 2, each line of a schedule file begins with an integer specifying the percentage of the time
available (which can be set using the −−timeout command line option) for which to run the




                                                         99
                                            Axiom                                                                   Axiom
                {}, M , [¬p, ¬q(_1)], [p]                                                     {}, M , [¬r], [¬p]
           ()                               Red                               Axiom                                  Lem                           Axiom
                {p}, M , [¬p, ¬q(_1)], []            {}, M , [¬p], [¬q(_1)]                  {¬p}, M , [¬r], [¬p]           {}, M , [], [¬p, ¬r]
     (_1 ← c)                                                                 Ext       ()                                                         Ext
                                   {¬q(_1)}, M , [¬p], []                                                   {¬r}, M , [], [¬p]
                              ()                                                                                                 Ext
                                                                     {¬p, ¬r}, M , [], []
                                                                                             Start
                                                                          ǫ, M , ǫ, ǫ



Figure 3: LATEX output for Example 1. Variables of the form _1, _2, . . . are fresh variables introduced by
the Start or Extension rules. Annotations to the left of a rule, such as (_1 ← c), denote substitutions
applied to the entire proof.


                                                                                               proof_stack([
                                                                                                   start(0),
                                                                                                   left_branch(0, 2, 0, 2),
                                                                                                   left_branch(0, 1, 1, 3),
                                                                                                   reduction(0, 0),
                                                                                                   right_branch(3),
                                                                                                   right_branch(2),
          matrix(0, [ -p, -r ]).                                                                   left_branch(0, 3, 1, 3),
          matrix(1, [ p, q(c) ]).                                                                  lemmata(0, 0),
          matrix(2, [ p, -q(X) ]).                                                                 right_branch(3)
          matrix(3, [ -p, r ]).                                                                ]).
          matrix(4, [ -p, q(a) ]).




    (a) Prolog-readable representation of the matrix.                                    (b) Stack representation of the proof.

Figure 4: Certificate for the proof of Example 1.


following settings (or 0 in the last line denoting “all time remaining”). By default, Connect++
runs in essentially the same way as the underlying leanCoP search, choosing proof steps on the
basis of the first available literal, and restricting backtracking in the same way. This default
behaviour is set at each line of the schedule, and the schedule line then modifies it. The flags in
the schedule line are named in the same way as the command line options; all command line
options that affect the search are available to a schedule file.
   Connect++ can produce a readable proof via LATEX. Example 1 is a problem from [6].
Example 1. M = {{¬P, ¬R}, {P, Q(c)}, {P, ¬Q(x)}, {¬P, R}, {¬P, Q(a)}} .
Figure 3 shows the typeset output for a proof of Example 1.
   Connect++ can output a simply-formatted proof certificate. While there is currently no
consensus on what format a certificate should take, suggestions have appeared [27, 8, 28] and
a proposal for a standard is given in [29]. Figure 4 shows a certificate for the proof shown in
Figure 3. It consists of Prolog-readable summaries of the matrix and a stack representation
of the proof (see Section 4). Each element of the stack describes the proof rule employed,
with left_branch and right_branch denoting the left and right premises of the Extensions.
Numbers after an item identify the element(s) used in applying a rule; clauses are indexed
from 0 in the matrix and literals are indexed from 0 within clauses. For example, referring
again to Figure 1, left_branch(0, 2, 0, 2) denotes that there is an Extension rule. The first
index denotes that L = ¬P (the 0-indexed literal in the clause C ∪ {L}).4 The second index
4
    Readers familiar with leanCoP might find this unusual. leanCoP always uses the leftmost literal in C ∪ {L} as the




                                                                         100
denotes that C ′ is a copy of {P, ¬Q(x)} (the 2-indexed clause in the matrix). The third index
denotes that L′ = P (the 0-indexed literal in the copy of C ′ ). The fourth number denotes the
depth within the proof. A short Prolog program reads this certificate and verifies that the rule
has been correctly applied at each stage, using the built-in unification mechanism to build the
substitution.


4. Implementation: some technical details
The requirements for compiling Connect++ are light. Aside from a C++ compiler, it uses the
Boost libraries5 for parsing TPTP and schedule files, and dealing with command-line parameters.
LATEX is needed for readable proofs and SWI Prolog [30] is needed for verifying proofs.
   Connect++ exploits the structure of the connection calculus by using an optimized rep-
resentation for variables and terms. As substitutions apply to an entire proof, any variable
is only represented once, and terms using that variable do so via a pointer. Any substitution
applied to a variable therefore takes effect everywhere the variable appears, in constant time,
and backtracking (removing a substitution) is equally fast and straightforward. Fresh variables
are recycled to preserve memory. Terms are constructed using pointers to subterms; subterms
are shared and no copy of an existing subterm is ever made. This is supported by an index: new
(sub)terms are added to the index and only stored if not already present; if already present then
a pointer to the existing copy is provided. Literals are straightforward identifiers paired with a
list of pointers to terms. Clauses are lists of literals. The matrix is indexed to allow fast lookup
of which clauses contain a literal, and the position of that literal in each relevant clause. This
aids fast identification of possible Extensions.
   As one aim of Connect++ is to provide flexibility in the proof search, it avoids the use of
recursion in favour of an iterative approach using a pair of stacks. Figure 5 illustrates this. The
proof is built in the left stack, and as left premises of Extensions are explored first, the right
stack is used to store the currently outstanding right premises. Stack items store C, P and L, a
substitution, and a list of actions (applications of the proof rules) that can be used to further
extend the proof at this point. This structure is manipulated iteratively, and as at any point there
is direct access to the list of possible actions stored in each stack item, there is great flexibility
in directing the search—the action list in each stack item can arbitrarily be re-ordered, added
to (increasing the degree of backtracking) or reduced (restricting the degree of backtracking)
while a proof is in progress.
   Planned developments to Connect++ include: (1) completion of clause translation, including
definitional clausal form, from TPTP first-order format; (2) enumeration of different proofs
for a single problem as a means of generating training data; (3) addition of other heuristics
for connection provers; (4) experiments with new heuristics; (5) addition of further command-
line options, and where appropriate inclusion of these in the system for handling schedules;
(6) implementation of readable proofs similar to those produced by leanCoP version 2.1; (7)
  principal literal, and at each stage only uses that literal to generate possible new steps for the proof tree. Connect++
  does the same in its default settings, but future development is planned allowing the choice of this literal to be
  subject to one or more heuristics, with the aim of ordering the search more effectively. The format of the certificate
  supports this planned extension.
5
  https://www.boost.org/




                                                          101
                                Axiom                                                          Axiom


                                Red3                                                           Red3
                                                                      Axiom
              Axiom             Red2                                  Red3     Axiom           Red2
                                                                      Red2
               Red1             ExtL3           ExtR3                 ExtL3     Red1           ExtL3           ExtR3
                                                                      ExtR2
    Axiom     ExtL2                     ExtR2                         Axiom    ExtL2                   ExtR2
     Red1                                                             Red1
    ExtL2               ExtL1                           ExtR1         ExtL2            ExtL1                           ExtR1
    ExtL1    ExtR2                                                    ExtL1   ExtR3
     Start   ExtR1                      Start                         Start   ExtR1                    Start




(a) Early in a proof search—the shaded area is not (b) After generating the shaded area, explore
    yet explored.                                      ExtR3.

Figure 5: Proof search arranged around two stacks. The proof itself is built on the left-hand stack, while
the right-hand stack maintains details of the currently outstanding right premises for Extensions.


implementation of any forthcoming standard for proof certificates; and (8) implementation of
better approaches to equality.


5. Evaluation
While a large-scale study of the power of Connect++ in comparison with other connection
provers, and across a large collection of problems, remains for future work, we provide some
brief, initial experimental results to demonstrate the prover in its current state.
   A selection of 52 AGT problems from TPTP version 8.0.06 were converted to a format readable
by Connect++.7 Connect++ was run8 on these problems using its default schedule (Figure 2)
and a 10 second timeout, on two systems: a MacBook Air M1 with 16GB memory running OS
X Sonoma, and the University of Cambridge High-Performance Computing (HPC) Facility.9
Figure 6 shows the running times for the problems solved by Connect++ within the 10 second
timeout.
   For comparison, running10 leanCoP version 2.1 with ECLiPSe version 5.10 #147 on the HPC,
again with the timeout set to 10 seconds and with the problems in first-order TPTP format11 , it is
clear that leanCoP can solve the same problems, and some others. However at this stage further
comparison is complicated as the systems have significant differences. In particular, leanCoP
has a significantly more detailed schedule employing various forms of clause translation, most
significantly definitional clausal form.

6
    Selected using: tptp2T -pp Domains AGT Form FOF Status Theorem Equality.
7
    tptp2X with options -tclausify:tptp -f tptp followed by a second run with options -tadd_equality -f
    tptp.
8
    ./connect++ --schedule default -v0 --no-equality --timeout 10 file.tptp
9
    Technical details for the Ice Lake CPUs employed can be found at https://www.hpc.cam.ac.uk/.
10
     ./leancop.sh file.tptp 10
11
     tptp2X with option -f tptp




                                                                102
Figure 6: Running times for Connect++ on two architectures for the AGT problems solved with a 10
second timeout and the default schedule. Names on the x-axis identify AGT problems when appended
to the prefix ‘AGT0’.


Acknowledgments
This work was performed using resources provided by the Cambridge Service for Data Driven
Discovery (CSD3) operated by the University of Cambridge Research Computing Service
(www.csd3.cam.ac.uk), provided by Dell EMC and Intel using Tier-2 funding from the En-
gineering and Physical Sciences Research Council (capital grant EP/T022159/1), and DiRAC
funding from the Science and Technology Facilities Council (www.dirac.ac.uk).




                                              103
References
 [1] S. B. Holden, Machine Learning for Automated Theorem Proving: Learning to Solve SAT
     and QSAT, volume 14 of Foundations and Trends® in Machine Learning, now publish-
     ers, Boston, Delft, 2021. URL: https://www.nowpublishers.com/article/Details/MAL-081.
     doi:10.1561/2200000081.
 [2] N. Eén, N. Sörensson, An extensible SAT-solver, in: E. Giunchiglia, A. Tacchella (Eds.), Pro-
     ceedings of the 6th International Conference on Theory and Applications of Satisfiability
     Testing, volume 2919 of Lecture Notes in Computer Science, Springer, 2003, pp. 502–518.
 [3] S. Schulz, E—a brainiac theorem prover, AI Communications 15 (2002) 111–126.
 [4] A. Riazanov, A. Voronkov, The design and implementation of VAMPIRE, AI Communica-
     tions 15 (2002) 91–110.
 [5] J. Otten, W. Bibel, leanCoP: lean connection-based theorem proving, Journal of Symbolic
     Computation 36 (2003) 139–161.
 [6] J. Otten, Restricting backtracking in connection calculi, AI Communications 23 (2010)
     159–182.
 [7] C. Kaliszyk, Efficient low-level connection tableaux, in: H. D. Nivelle (Ed.), 24th Interna-
     tional Conference on Automated Reasoning with Analytic Tableaux and Related Methods
     (TABLEAUX 2015), volume 9323 of Lecture Notes in Artificial Intelligence, Springer, 2015,
     pp. 102–111.
 [8] C. Kaliszyk, J. Urban, J. Vyskočil, Certified connection tableaux proofs for HOL Light and
     TPTP, in: Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP),
     Association for Computing Machinery, New York, NY, United States, 2015, pp. 59–66.
 [9] M. Färber, C. Kaliszyk, J. Urban, Machine learning guidance for connection tableax, Journal
     of Automated Reasoning 65 (2021) 287–320.
[10] M. Färber, cop: Highly efficient first-order connection proving, 2021. URL: https://lib.rs/
     crates/cop.
[11] F. Rømming, J. Otten, S. B. Holden, Markov decision processes for classical, intuition-
     istic, and modal connection calculi, 2023. Submitted to the International Workshop on
     Automated Reasoning with Connection Calculi (AReCCA) 2023.
[12] G. Prusak, C. Kaliszyk, Lazy paramodulation in practice, in: B. Konev, C. Schon, A. Steen
     (Eds.), Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR),
     volume 3201 of CEUR Workshop Proceedings, 2022.
[13] V. Toth, Reinforcement Learning for Automated Theorem Proving, Master’s thesis, Uni-
     versity of Cambridge, Department of Computer Science and Technology, The Computer
     Laboratory, William Gates Building, 15 JJ Thomson Avenue, Cambridge, CB3 0FD, 2021.
[14] Z. Zombori, A. Csiszárik, H. Michalewski, C. Kaliszyk, J. Urban, Towards finding longer
     proofs, in: A. Das, S. Negri (Eds.), Proceedings of the International Conference on Au-
     tomated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), volume
     12842 of Lecture Notes in Artificial Intelligence, Springer, 2021, pp. 167–186.
[15] M. Färber, A curiously effective backtracking strategy for connection tableaux, 2021.
     ArXiv:2106.13722v1 [cs.LO].
[16] T. Raths, J. Otten, randoCoP: Randomizing the proof search order in the connection
     calculus, in: B. Konev, R. A. Schmidt, S. Schulz (Eds.), Proceedings of the First International




                                               104
     Workshop on Practical Aspects of Automated Reasoning (PAAR), volume 373 of CEUR
     Workshop Proceedings, 2008.
[17] R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd edition ed., MIT
     Press, 2018.
[18] C. B. Browne, E. Powley, D. Whitehouse, S. M. Lucas, P. I. Cowling, P. Rohlfshag, S. Tavener,
     D. Perez, S. Samothrakis, S. Colton, A survey of Monte Carlo tree search methods, IEEE
     Transactions on Computational Intelligence and AI in Games 4 (2012) 1–43.
[19] B. E. Oliver, J. Otten, Equality preprocessing in connection calculi, in: P. Fontaine,
     K. Korovin, I. S. Kotsireas, P. Rümmer, S. Tourret (Eds.), Proceedings of the 7th Workshop
     on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking
     and Symbolic Computation Workshop (SC-Square) Workshop, volume 2752 of CEUR
     Workshop Proceedings, 2020.
[20] G. Prusak, C. Kaliszyk, Lazy paramodulation in practice, in: B. Konev, C. Schon, A. Steen
     (Eds.), Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning
     (PAAR), volume 3201 of CEUR Workshop Proceedings, 2022.
[21] G. Sutcliffe, C. Suttner, The TPTP problem library for automated theorem proving, 2023.
     URL: https://tptp.org/.
[22] F. Hutter, H. H. Hoos, K. Leyton-Brown, T. Stützle, Paramils: An automatic algorithm
     configuration framework, Journal of Artificial Intelligence Research 36 (2009) 267–306.
[23] F. Hutter, H. H. Hoos, K. Leyton-Brown, Sequential model-based optimization for general
     algorithm configuration, in: C. A. C. Coello (Ed.), Proceedings of the 5th International
     Conference on Learning and Intelligent Optimization (LION), volume 6683 of Lecture Notes
     in Computer Science, Springer, 2011, pp. 507–523.
[24] C. Ansótegui, M. Sellmann, K. Tierney, A gender-based genetic algorithm for the automatic
     configuration of algorithms, in: I. P. Gent (Ed.), Proceedings of the 15th International
     Conference on Principles and Practice of Constraint Programming (CP), volume 5732 of
     Lecture Notes in Computer Science, Springer, 2009, pp. 142–157.
[25] C. Mangla, S. B. Holden, L. Paulson, Bayesian optimisation of solver parameters in
     CBMC, in: F. Bobot, T. Weber (Eds.), Proceedings of the 18th International Workshop on
     Satisfiability Modulo Theories (SMT), volume 2854, CEUR Workshop Proceedings, 2020,
     pp. 37–47. URL: http://ceur-ws.org/Vol-2854/.
[26] C. Mangla, S. B. Holden, L. Paulson, Bayesian ranking for strategy scheduling in automated
     theorem provers, in: J. Blanchette, L. Kovács, D. Pattinson (Eds.), Proceedings of the
     11th International Joint Conference on Automated Reasoning (IJCAR), volume 13385
     of Lecture Notes in Artificial Intelligence, Springer, 2022, pp. 559–577. URL: https://link.
     springer.com/chapter/10.1007/978-3-031-10769-6_33. doi:https://doi.org/10.1007/
     978-3-031-10769-6.
[27] J. Otten, G. Sutcliffe, Using the TPTP language for representing derivations in tableau and
     connection calculus, volume 9 of EPiC Series, 2012, pp. 95–105.
[28] M. Färber, C. Kaliszyk, J. Urban, Machine learning guidance and proof certification for
     connection tableaux, 2018. ArXiv:1805.03107v3 [cs.LO].
[29] J. Otten, S. B. Holden, A standardized syntax for connection proofs, 2023. Submitted to
     the International Workshop on Automated Reasoning with Connection Calculi (AReCCA)
     2023.




                                               105
[30] J. Wielemaker, T. Schrijvers, M. Triska, T. Lager, SWI-Prolog, Theory and Practice of Logic
     Programming 12 (2011) 67–96.




                                              106