=Paper= {{Paper |id=Vol-3613/AReCCa2023_paper1 |storemode=property |title=20 Years of leanCoP - An Overview of the Provers |pdfUrl=https://ceur-ws.org/Vol-3613/AReCCa2023_paper1.pdf |volume=Vol-3613 |authors=Jens Otten |dblpUrl=https://dblp.org/rec/conf/arecca/Otten23 }} ==20 Years of leanCoP - An Overview of the Provers== https://ceur-ws.org/Vol-3613/AReCCa2023_paper1.pdf
                                20 Years of leanCoP — An Overview of the Provers
                                Jens Otten*
                                Department of Informatics, University of Oslo, Norway


                                                                      Abstract
                                                                      This paper gives a comprehensive overview of the automated theorem prover leanCoP and all its
                                                                      variants for classical and non-classical first-order logics that have been developed so far. It includes
                                                                      historical details describing how seven lines of Prolog code turned into some of the most popular and
                                                                      efficient connection provers for classical and non-classical logics. The paper provides an overview of the
                                                                      non-clausal version nanoCoP and other implementations inspired by leanCoP.

                                                                      Keywords
                                                                      leanCoP, connection calculus, classical logic, automated reasoning, non-classical logics




                                1. Introduction
                                Automating formal reasoning is a core research field in Artificial Intelligence. One of its main
                                goals is to develop efficient (theorem) provers that automate the search for a formal proof of a
                                given conjecture with respect to a specific logic.
                                   20 years ago, the article “leanCoP: Lean Connection-based Theorem Proving” [1] started the
                                development of a series of compact theorem provers for classical and several non-classical logics.
                                The very first version of leanCoP was written a few years earlier, in November 1999, when the
                                author was asked by Wolfgang Bibel to take on a lecture of his course “Inferenzmethoden” at
                                TU Darmstadt, because he was out of town. The intent of this prover was to show students a
                                compact Prolog implementation of the (classical) connection calculus [2, 3] which was the topic
                                of the lesson at that time. Slightly simplifying that code and adding the positive start clause
                                technique resulted in leanCoP 1.0, whose seven lines of Prolog code is shown in the abstract
                                of the 2003 leanCoP article. Since then, several connection provers based on or inspired by
                                leanCoP have been developed by the author as well as by many other researchers.
                                   This paper provides a comprehensive overview of the leanCoP connection provers and all
                                its siblings that have been developed so far. The leanCoP provers for classical first-order logic
                                (Section 2) are the foundation for all subsequent provers. ileanCoP (Section 3) and MleanCoP
                                (Section 4) are versions of leanCoP for first-order intuitionistic and modal logics, respectively;
                                they use prefixes to encode the Kripke semantics of these non-classical logics. nanoCoP is a
                                generalization of leanCoP and works on formulae in non-clausal form (Section 5). The paper
                                also presents an overview of implementations based on or inspired by leanCoP (Section 6)
                                before concluding with a brief summary (Section 7).
                                AReCCa 2023: Automated Reasoning with Connection Calculi, 18 September 2023, Prague, Czech Republic
                                $ jeotten@ifi.uio.no (J. Otten)
                                € http://jens-otten.de/ (J. Otten)
                                 0000-0002-4331-8698 (J. Otten)
                                                                    © 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                                                                                             4                                                           CEUR-WS.org




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
            prove(M,I) :- append(Q,[C|R],M), \+member(-_,C),
             append(Q,R,S), prove([!],[[-!|C]|S],[],I).
            prove([],_,_,_).
            prove([L|C],M,P,I) :- (-N=L; -L=N) -> (member(N,P);
             append(Q,[D|R],M), copy_term(D,E), append(A,[N|B],E),
             append(A,B,F), (D==E -> append(R,Q,S); length(P,K), K prove([-(#)],[],I,[],S) ;
                   lit(#,C,_) -> prove(C,[-(#)],I,[],S).
               prove(I,S) :- member(comp(L),S), I=L -> prove(1,[]) ;
                   (member(comp(_),S);retract(p)) -> J is I+1, prove(J,S).
               prove([],_,_,_,_).
               prove([L|C],P,I,Q,S) :- \+ (member(A,[L|C]), member(B,P),
                   A==B), (-N=L;-L=N) -> ( member(D,Q), L==D ;
                   member(E,P), unify_with_occurs_check(E,N) ; lit(N,F,H),
                   (H=g -> true ; length(P,K), K true ;
                   \+p -> assert(p), fail), prove(F,[L|P],I,Q,S) ),
                   (member(cut,S) -> ! ; true), prove(C,P,I,[L|Q],S).


Figure 3: The minimal source code of the leanCoP 2.0 prover for classical first-order logic.


2.3. leanCoP 2.0
Even though leanCoP 1.0 already outperformed the famous Otter theorem prover [10] on a small
number of problems [1], the development of the next version took a big step forward. In the year
2006, the problems of the MPTP challenge [11] motivated the integration of further optimizations
into leanCoP: regularity, lemmata, restricted backtracking, conjecture start clauses, definitional
clausal form, strategy scheduling and a more efficient representation of the input clauses. It
resulted in leanCoP 2.0, whose minimal Prolog code of the core prover is shown in Fig. 3.5 This
minimal version of leanCoP 2.0 is still only 555 bytes in size.
   A few basic but effective techniques were carefully selected and integrated into leanCoP 2.0.
Regularity reduces the search space by ensuring that no literal occurs more than once on the
active path [5]. Lemmata (or factorization) reuses the subproof of a literal in order to solve the
same literal at a later point in the proof search [5]. Restricted backtracking is an effective (but
incomplete) technique to prune the search space in the (non-confluent) connection calculus [12].
It cuts off any alternative applications of reduction and extensions rules once a literal from
the subgoal clause has been solved.6 Furthermore, backtracking can also be restricted when
selecting the clause C1 in the start rule by omitting alternative start clauses. Conjecture start
clauses restrict the start rule for formulae of the form (A1 ∧ . . . ∧ An ) ⇒ C to clauses of the
conjecture C instead of the (default) positive clauses. A definitional clausal form translation,
which is done in a preprocessing step, introduces definitions for certain subformulae [12],
hereby reducing the size of the resulting matrix. Reordering clauses is done in a preprocessing
step and modifies (indirectly) the proof search order, by reordering the clauses in the input
matrix. Strategy scheduling uses a sequence of different strategies to prove a formula, which are
specified in the last argument of the prove predicate [13, 12]. For example, the first strategy
“[cut,comp(7)]” used by leanCoP 2.0 uses restricted backtracking and restarts with a complete
proof search (without restricted backtracking) if a proof depth of 7 is reached [12].

5
  The source code shown in Fig. 3 uses only standard (built-in) Prolog predicates and implements the whole proof
  search. The input matrix is stored in Prolog’s database using the lit predicate (see below for details).
6
  The literal L1 in Fig. 2 is called solved; in case of the extension rule, there also has to be a proof for the left premise.




                                                              7
   Using a lean Prolog technology [12], the clauses of the input matrix M are stored in Prolog’s
database in a preprocessing step. For every clause C ∈ M and for all literals L ∈ C the fact
“lit(L,C1,Grnd).” is stored, where C1=C\{L} and Grnd is g if C is ground (does not contain
any variables) and n, otherwise. This integrates the main advantage of the ”Prolog technology”
approach [14] into leanCoP, using Prolog’s fast indexing mechanism to find connections.
   Fig. 4 (ignoring the underlined code) shows the comprehensive source code of leanCoP 2.0.
The core prover is invoked with prove(1,Set), where Set is a strategy and the initial limit
for the proof depth (size of the active path) is 1. This predicate succeeds iff there is a connection
proof for the matrix/clauses stored in Prolog’s database. The proof search starts by applying
the start rule (lines a–c). The path limit is used to perform iterative deepening on the size of the
active path (lines e–h), which is necessary for completeness. Afterwards, the reduction rule
(lines 2, 5, 8, 17) and the extension rule (lines 2, 5, 11–14, 17) are repeatedly applied, until the
branch in the derivation can be closed by an axiom (line 1). A controlled iterative deepening stops
the proof search if the current path limit for the size of the active path is not exceeded (line g and
13). This yields a decision procedure for ground (e.g. propositional) formulae and also allows for
refuting some (invalid) first-order formulae. The proof search optimizations integrated into the
core prover are regularity (line 4), lemmata (line 6), and restricted backtracking (line 16); see [12]
for details. The term substitution σT is stored implicitly by Prolog. The additional optimizations
improve the performance of leanCoP significantly, in particular for large formulae [12].


        (a)      prove(PathLim,Set,Proof) :-
        (b)          \+member(scut,Set) -> prove([-(#)],[],PathLim,[],Set,[Proof]) ;
        (c)          lit(#,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1),
        (d)          Proof=[C|Proof1].
        (e)      prove(PathLim,Set,Proof) :-
        (f)          member(comp(Limit),Set), PathLim=Limit -> prove(1,[],Proof) ;
        (g)          (member(comp(_),Set);retract(pathlim)) ->
        (h)          PathLim1 is PathLim+1, prove(PathLim1,Set,Proof).
        (1)      prove([],_,_,_,_,[]).
        (2)      prove([Lit|Cla],Path,PathLim,Lem,Set,Proof) :-
        (3)          Proof=[[[NegLit|Cla1]|Proof1]|Proof2],
        (4)          \+ (member(LitC,[Lit|Cla]), member(LitP,Path), LitC==LitP),
        (5)          (-NegLit=Lit;-Lit=NegLit) ->
        (6)             ( member(LitL,Lem), Lit==LitL, Cla1=[], Proof1=[]
        (7)               ;
        (8)               member(NegL,Path), unify_with_occurs_check(NegL,NegLit),
        (9)               Cla1=[], Proof1=[]
       (10)               ;
       (11)               lit(NegLit,Cla1,Grnd1),
       (12)               ( Grnd1=g -> true ; length(Path,K), K true ;
       (13)                 \+ pathlim -> assert(pathlim), fail ),
       (14)               prove(Cla1,[Lit|Path],PathLim,Lem,Set,Proof1)
       (15)             ),
       (16)             ( member(cut,Set) -> ! ; true ),
       (17)             prove(Cla,Path,PathLim,[Lit|Lem],Set,Proof2).


Figure 4: The source code of the leanCoP 2.0 and leanCoP 2.1/2.2 provers for classical first-order logic.




                                                   8
Table 1
leanCoP 2.0 and ileanCoP 1.2 at CASC 2007.

                     Prover             proved      refuted     rating >0.68       CASC package size
                     Vampire 9.0           270            -               59                7700 kB
                     E 0.999               248            -               41               17800 kB
                     iProver 0.2           201            -               18                5800 kB
                     Equinox 1.2           173            -               19                6200 kB
                     leanCoP 2.0           160            -               21                 26 kB
                     Otter 3.3             138            -                6                3200 kB
                     Metis 2.0             117            -                2               13700 kB
                     Geo 2007f             104            -                5                6400 kB
                     ileancop 1.2          103            9               13                 27 kB
                     Muscadet 2.7           37            -               11                3000 kB

   At CASC in 2007, leanCoP 2.0 [13, 12] proved more problems (out of 300 problems with a
time limit of 360 seconds) than four other provers in the main FOF division [15], including 21
“difficult” problems; see Table 1. It proved four problems not solved by the Vampire prover [16],
won both the bushy and chainy 100$ MPTP challenges, and was awarded Best Newcomer [15].
Example 3. The preprocessing step of leanCoP 2.0 stores the clauses of matrix M1 from Example 1,
M1 = {{¬man (Plato)}, {man (x), ¬mortal (x)}, {mortal (Plato)}}, in the following form:7
     lit(#,[mortal(plato)],g). (clause 3)                          lit(man(X),[-mortal(X)],n). (clause 2)
     lit(mortal(plato),[#],g). (clause 3)                          lit(-mortal(X),[man(X)],n). (clause 2)
     lit(-man(plato),[],g).    (clause 1)
Then when the leanCoP 2.0 prover is invoked with “ prove(1,[cut,comp(7)]).” it returns
“yes”. Therefore, the matrix M1 as well as the original formula F1 are valid (in classical logic).

2.4. leanCoP 2.1/2.2
In leanCoP 2.1 a few additional features have been added to leanCoP 2.0. leanCoP 2.1 directly
supports the TPTP input syntax (for FOF) with equality, where equality axioms are automatically
added if necessary. The fixed strategy scheduling is now controlled by a shell script, and support
for SWI and SICStus Prolog is added. Furthermore, an additional Proof argument is added
to the core prover, which returns a compact connection proof. Afterwards, this proof can be
translated into different formats: connect (standard connection proof), leantptp (proof in
a TPTP-like syntax) and readable (readable proof in natural language). In leanCoP 2.2 the
(detailed) proof output has been improved and the fixed strategy scheduling optimized.
   The source code of the leanCoP 2.1/2.2 core prover is shown in Fig. 4. The underlined code,
which collects the proof, was added to leanCoP 2.0, nothing else was changed. The core prover
is invoked with prove(1,Set,Proof), where Proof returns the found connection proof.
   At CASC in 2009, the leanCoP 2.1 prover, and at CASC in 2010, the leanCoP 2.2 prover were
among the top three provers that return a proof in the main FOF division.8
7
    The special literal # is added to all positive clauses and the proof starts with the subgoal [-(#)] (line b/c in Fig. 4).
8
    See https://www.tptp.org/CASC/J5/ and https://www.tptp.org/CASC/22/




                                                               9
Example 4. For the matrix M1 stored as shown in Example 3, the leanCoP 2.1/2.2 core prover
invoked with “ prove(1,[cut,comp(7)],Proof).” returns the compact connection proof
    Proof = [[#,mortal(plato)],[[-(mortal(plato)),man(plato)],[[-(man(plato))]]]]
which is a nested list of clauses C2 used in start/extension steps (or literals L2 in reduction steps).


3. ileanCoP — Intuitionistic Logic
Intuitionistic logic [17] has applications, e.g., in program synthesis and within interactive proof
assistants such as Coq [18] and NuPRL [19] used for constructing provably correct software.
Intuitionistic and classical logic share the same syntax, but their semantics is different. For
example, the formula man(Socrates) ∨ ¬man(Socrates) is valid in classical logic, but not in
intuitionistic logic. The semantics of intuitionistic logic requires a proof for man(Socrates) or
for ¬man(Socrates), which do not exist. Every formula that is valid in intuitionistic logic is
also valid in classical logic, but not vice versa. Gentzen already provided a sequent calculus
LJ for intuitionistic first-order logic [6]. Wallen extended Bibel’s matrix characterization [3] to
intuitionistic logic by using prefixes to encode the Kripke semantics [20]. This characterization,
originally formulated for formulae in non-clausal form, was adapted to clausal form by using
an extended Skolemization [21]. It serves as the basis for a clausal connection calculus for
intuitionistic first-order logic and the ileanCoP implementation [21].

3.1. The Intuitionistic Connection Calculus
For intuitionistic logic the matrix and the calculus are extended by prefixes, representing world
paths in the Kripke semantics; see [20, 22]. A prefix p is a string consisting of variables (denoted
by V ) and constants (denoted by a) and assigned to each literal (and subformula).

Definition 2. The intuitionistic matrix M (F pol :p) of a prefixed formula F pol :p with polarity
pol∈{0, 1} (see [7, 20]) is defined according to Table 2. MG ∪β MH := {CG ∪ CH | CG ∈ MG ,
CH ∈ MH }, x* is a new term variable, t* is the Skolem term f * (x1 , . . . , xn ), V * is a new prefix
variable, a* is the prefix constant f * (x1 , . . . , xn ), f * is a new function symbol and x1 , . . . , xn
are all free term and prefix variables in A0 : p, (¬G)0 : p, (G ⇒ H)0 : p, (∀xG)0 : p or (∃xG)1 : p,
respectively. The intuitionistic matrix M i (F ) of a formula F is the intuitionistic matrix M (F 0 : ε).

Table 2
The prefixed (clausal) matrix for intuitionistic logic.

      F pol : p      M (F pol : p)                            F pol : p    M (F pol : p)
      A0 : p         {{A0 : pa* }}                        β   (G∧H)0 : p   M (G0 : p) ∪β M (H 0 : p)
      A1 : p         {{A1 : pV * }}                           (G∨H)1 : p   M (G1 : p) ∪β M (H 1 : p)
α     (¬G)0 : p      M (G1 : pa* )                            (G⇒H)1 :p    M (G0 :pV * ) ∪β M (H 1 :pV * )
      (¬G)1 : p      M (G0 : pV * )                       γ   (∀xG)1 : p   M (G[x\x* ]1 : pV * )
      (G∧H)1 : p     M (G1 : p) ∪ M (H 1 : p)                 (∃xG)0 : p   M (G[x\x* ]0 : p)
      (G∨H)0 : p     M (G0 : p) ∪ M (H 0 : p)             δ   (∀xG)0 : p   M (G[x\t* ]0 : pa* )
      (G⇒H)0 :p      M (G1 :pa* ) ∪ M (H 0 :pa* )             (∃xG)1 : p   M (G[x\t* ]1 : p)




                                                     10
                                                              C2 , M, {}
      Axiom (A)                                   Start (S)                     C2 is a copy of C1 ∈M
                   {}, M, P ath                                ε, M, ε

                      C, M, P ath∪{L2 : p2 }
  Reduction (R)                                          {L1 : p1 , L2 : p2 } is σ-complementary
                   C∪{L1 : p1 }, M, P ath∪{L2 : p2 }

                   C2 \{L2 : p2 }, M, P ath∪{L1 : p1 } C, M, P ath         C2 is a copy of C1 ∈M ,
   Extension (E)                                                           L2 : p2 ∈C2 , {L1 : p1 , L2 : p2 }
                                  C∪{L1 : p1 }, M, P ath                   is σ-complementary

Figure 5: The clausal connection calculus for intuitionistic and modal logic.


  A prefix substitution σP assigns strings to prefix variables and is calculated by a prefix
unification [21]. In intuitionistic logic, a connection {A01 : p1 , A12 : p2 } is σ-complementary iff
σT (A1 ) = σT (A2 ) and σP (p1 ) = σP (p2 ) for a combined substitution σ = (σT , σP ).

Definition 3 (Clausal Connection Calculus for Intuitionistic Logic). The (clausal) con-
nection calculus for intuitionistic logic [21] is given in Fig. 5. An intuitionistic connection
proof for F is a derivation of ε, M i (F ), ε with an admissible (see [20, 21]) combined substitution
σ = (σT , σP ), in which all leaves are axioms.

Example 5. The intuitionistic matrix of the formula F1 from Example 1 is M1i = M i (F1 ) =
{{man(Plato)1 : a1 V1 }, {man(x)0 : a1 V2 a2 (x), mortal(x)1 : a1 V2 V3 }, {mortal(Plato)0 : a1 a3 }}.
The intuitionistic connection proof for M1i uses the same steps as the classical proof in Exam-
ple 2, but with a combined substitution σ = (σT , σP ) with σT (x′ ) = Plato, σP (V1 ) = a2 (Plato),
σJ (V2 ) = ε and σP (V3 ) = a3 (where ε is the empty string). Therefore, M1i and F1 are valid in intu-
itionistic logic. The intuitionistic matrix of the formula F2 = man(Socrates) ∨ ¬ man(Socrates) is
M2i = M i (F2 ) = {{man(Socrates)0 : a1 }, {man(Socrates)1 : a2 }}. It contains the only connection
{man(Socrates)0 : a1 , man(Socrates)1 : a2 }, which cannot be complementary as there is no σP
that unifies the two prefixes a1 and a2 . Therefore, M2i and F2 are not valid in intuitionistic logic.

3.2. ileanCoP 1.0/1.2
ileanCoP is a compact Prolog implementation of the clausal connection calculus for intuitionistic
logic and extends the classical connection prover leanCoP by (a) prefixes (that are added to the
literals in the matrix in a preprocessing step), (b) a set of prefix equations (that are collected
during the proof search), (c) a set of term variables (with their prefixes) assigned to each clause
(in order to check the admissibility of σ, also called domain condition), and (d) a prefix unification
algorithm (that unifies the prefixes of the literals in each connection).
   ileanCoP 1.0 [21] is based on (classical) leanCoP 1.0 and implements the basic intuitionistic
connection calculus. ileanCoP 1.2 [13] integrates all the additional optimization techniques and
strategies of leanCoP 2.0. The minimal source code of the ileanCoP 1.2 core prover is shown in
Fig. 6. The underlined code was added to the classical prover leanCoP 2.0 shown in Fig. 3; no
further changes were made. In a preprocessing step the clauses of the intuitionistic matrix are
written into Prolog’s database using the lit predicate (see also Section 2.3).




                                                  11
        prove(I,S) :- ( \+member(scut,S) ->
            prove([(-(#)):(-[])],[],I,[],[Z,T],S) ;
            lit((#):_,G:C,_) -> prove(C,[(-(#)):(-[])],I,[],[Z,R],S),
            append(R,G,T) ), domain_cond(T), prefix_unify(Z).
        prove(I,S) :- member(comp(L),S), I=L -> prove(1,[]) ;
            (member(comp(_),S);retract(p)) -> J is I+1, prove(J,S).
        prove([],_,_,_,[[],[]],_).
        prove([L:U|C],P,I,Q,[Z,T],S) :- \+ (member(A,[L:U|C]), member(B,P),
            A==B), (-N=L;-L=N) -> ( member(D,Q), L:U==D, X=[], O=[] ;
            member(E:V,P), unify_with_occurs_check(E,N),
            \ + \ + prefix_unify([U=V]), X=[U=V], O=[] ;
            lit(N:V,M:F,H), \ + \ + prefix_unify([U=V]),
            (H=g -> true ; length(P,K), K true ;
            \+p -> assert(p), fail), prove(F,[L:U|P],I,Q,[W,R],S),
            X=[U=V|W], append(R,M,O) ), (member(cut,S) -> ! ; true),
            prove(C,P,I,[L:U|Q],[Y,J],S), append(X,Y,Z), append(J,O,T).

Figure 6: The source code of the ileanCoP 1.2/MleanCoP 1.2 core provers for intuitionistic/modal logic.

   The prover is invoked with prove(1,S), where S is a strategy (see Section 2.3) and the
start limit for the size of the active path is 1. The predicate succeeds if there is an intuition-
istic connection proof for the stored input clauses. First, ileanCoP performs a classical proof
search. After a classical proof is found, the domain condition is checked and the prefixes of
the literals in each connection are unified [21]. This is done by the predicates domain_cond
and prefix_unify, respectively, in the fourth line of the code in Fig. 6. These are the only
additional predicates invoked during the proof search and are implemented by 5 and 21 lines of
Prolog code, respectively. The substitutions σT and σP are stored implicitly by Prolog.
   At CASC in 2007, see Table 1, ileanCoP 1.2 [13] proved two problems intuitionistically that
Vampire [16] did not prove classically even though reasoning in intuitionistic logic is significantly
harder (for propositional logic it is PSPACE-complete [23] compared to NP-complete [24]). For
more than 10 years ileanCoP 1.2 was the fastest prover for intuitionistic first-order logic.


4. MleanCoP — Modal Logic
Modal logics [25, 26] are among the most popular non-classical logics and have applications in,
e.g., planning, natural language processing, and program verification. Modal logics extend the
language of classical logic with the unary modal operators □ and ♢ representing the modalities
”it is necessarily true that” and ”it is possibly true that”, respectively. For example, the proposition
“if Plato is necessarily a man, then Plato is possibly a man” can be represented by the modal
formula □ man(Plato) ⇒ ♢ man(Plato) .
    The Kripke semantics of the (standard) modal logics is defined by a set of worlds and a binary
accessibility relation between these worlds. In each single world the classical semantics applies
to the classical connectives, whereas the modal operators □ and ♢ are interpreted with respect
to accessible worlds. There exist a broad range of different modal logics and the properties of
the accessibility relation specify the particular modal logic, such as D, T, S4 or S5.




                                                  12
Table 3
The prefixed (clausal) matrix for modal logic.

             F pol : p           M (F pol : p)                                F pol : p         M (F pol : p)
             Apol : p            {{Apol : p}}                             γ   (∀xG)1 : p        M (G[x\x* ]1 : p)
        α    (¬G)pol : p         M (G1−pol : p)                               (∃xG)0 : p        M (G[x\x* ]0 : p)
             (G∧H)1 : p          M (G1 : p) ∪ M (H 1 : p)                 δ   (∀xG)0 : p        M (G[x\t* ]0 : p)
             (G∨H)0 : p          M (G0 : p) ∪ M (H 0 : p)                     (∃xG)1 : p        M (G[x\t* ]1 : p)
             (G⇒H)0 : p          M (G1 : p) ∪ M (H 0 : p)                 ν   (□G)1 : p         M (G1 : pV * )
        β    (G∧H)0 : p          M (G0 : p) ∪β M (H 0 : p)                    (♢G)0 : p         M (G0 : pV * )
             (G∨H)1 : p          M (G1 : p) ∪β M (H 1 : p)                π   (□G)0 : p         M (G0 : pa* )
             (G⇒H)1 : p          M (G0 : p) ∪β M (H 1 : p)                    (♢G)1 : p         M (G1 : pa* )


  Proof calculi for modal logic often use prefixes [27] and so does Wallen’s matrix characteri-
zations [20]. Again, this characterization was adapted and serves as the basis for the clausal
connection calculus and the MleanCoP implementation for several modal logics [28, 29].9

4.1. The Modal Connection Calculus
For modal logic the matrix and the calculus are extended by prefixes, representing world paths
in the Kripke semantics; see [20, 22]. Again, a prefix p is a string consisting of variables (denoted
by V ) and constants (denoted by a) and assigned to each literal (and subformula).

Definition 4. The modal matrix M (F pol :p) of a prefixed formula F pol :p with polarity
pol∈{0, 1} is defined according to Table 3. MG ∪β MH := {CG ∪ CH | CG ∈ MG , CH ∈ MH },
x* is a new term variable, t* is the Skolem term f * (x1 , . . . , xn ), V * is a new prefix variable, a* is
the prefix constant f * (x1 , . . . , xn ), f * is a new function symbol and x1 , . . . , xn are all free term
and prefix variables in (∀xG)0 : p, (∃xG)1 : p, (□G)0 : p or (♢G)1 : p, respectively. The modal
matrix M m (F ) of a formula F is the modal matrix M (F 0 : ε).

   A prefix substitution σP assigns strings to prefix variables and is calculated by a prefix
unification [28, 31, 32]. In modal logic, a connection {A01 : p1 , A12 : p2 } is σ-complementary iff
σT (A1 ) = σT (A2 ) and σP (p1 ) = σP (p2 ) for a combined substitution σ = (σT , σP ). The prefix
unification procedure depends on the specific modal logic and its domain condition and has
to respect its accessibility condition: |σP (V )| = 1 for the modal logic D and |σP (V )| ≤ 1 for
the modal logic T (for all prefix variables V ); for S5 only the last character (or ε if the prefix is
empty) of each prefix has to be unified; there is no restriction for the modal logic S4 [28, 29].

Definition 5 (Clausal Connection Calculus for Modal Logic). The (clausal) connection
calculus for modal logic [28, 31] is given in Fig. 5. A modal connection proof for the modal
formula F is a derivation of ε, M m (F ), ε with an admissible (see [20, 28]) combined substitution
σ = (σT , σP ), in which all leaves are axioms.
9
    The calculus and the implementation for modal logic are very similar to the ones for intuitionistic logic in Section 3;
    only the specification of prefixes, the prefix unification and the domain condition differ. Indeed, Gödel showed that
    intuitionistic logic can be embedded into the modal logic S4 with cumulative domains [30]. For historical reasons
    and to keep the notation simple for different audiences, these logics are covered in separate sections.




                                                             13
Example 6. The modal matrix of F3 = □ man ⇒ □♢ man is M3m = M m (F3 ) = {{man1 :V1 },
{man0 :a1 V2 }}. The modal connection proof for M3m has one connection {man1 :V1 , man0 :a1 V2 },
which is σ-complementary for the combined (admissible) substitutions σP (V1 ) = a1 , σP (V2 ) = ε
(empty string) for T, σP (V1 ) = a1 V2 for S4, and σP (V1 ) = V2 for S5. Therefore, M3m and F3 are
valid in the modal logics T, S4 and S5, but not in the modal logic D (which requires |σP (Vi )| = 1).

4.2. MleanCoP 1.2/1.3
MleanCoP is a compact implementation of the connection calculus for the modal logics D, T,
S4 and S5 with constant, cumulative and varying domains. MleanCoP 1.2 [28] is based on
leanCoP 2.0 extended by prefixes and a prefix unification algorithm used to calculate the prefix
substitution σP . The minimal source code of the MleanCoP 1.2 core prover is shown in Fig. 6.
The underlined code was added to the classical prover, no further changes were made. In a
preprocessing step the clauses of the modal matrix are written into Prolog’s database using the
lit predicate (see also Section 2.3). The prover is invoked with prove(1,S), which succeeds
if there is a modal connection proof for the stored input clauses. After a classical proof is
found, the domain condition is checked (domain_cond) and the prefixes of the literals in each
connection are unified (prefix_unify), which depend on the specific modal logic [20, 28].
   MleanCoP 1.3 [29] includes the following improvements: support for heterogenous mul-
timodal logics, output of a compact modal connection proof, support for the modal QMLTP
input syntax [33] and an improved strategy scheduling. Up to the release of nanoCoP-M 2.0,
MleanCoP was the fastest prover for the first-order modal logics D, T, S4 and S5 [34, 35].

5. nanoCoP — Non-Clausal Reasoning
nanoCoP [31, 36, 37, 35] is a series of compact Prolog implementations of the non-clausal
connection calculus. The non-clausal connection calculus for classical [38, 39] and non-classical
logics [37] generalizes the clausal connection calculus [1, 2, 3].

5.1. The Non-Clausal Connection Calculus
In the clausal connection calculus a matrix is a set of clauses, where a clause is a set of literals.
The non-clausal connection calculus works on non-clausal matrices, in which a matrix is a set
of clauses and a clause is a set of literals and (sub)matrices. It can be seen as a representation of
a formula in negation normal form. For the non-classical logics, the non-clausal matrix and
calculus are extended by prefixes p, i.e., strings consisting of variables (V ) and constants (a).
Definition 6. The classical non-clausal matrix M (F pol ) of F pol with polarity pol ∈ {0, 1}
is defined (inductively) according to Table 4; the prefixes : p... and the last two lines are to be
ignored. The non-classical non-clausal matrix M i/m (F pol :p) of F pol :p with polarity pol ∈ {0, 1}
is defined (inductively) according to Table 4; for intuitionistic logic (M i ) the last two lines are to
be ignored, for modal logic (M m ) the underlined characters are to be ignored). x* is a new term
variable, t* is the Skolem term f * (x1 , . . . , xn ), V * is a new prefix variable, a* is the prefix constant
f * (x1 , . . . , xn ), f * is a new function symbol and x1 , . . . , xn are all free term and prefix variables
in the corresponding formula F pol : p. The classical non-clausal matrix M (F ) of F is the matrix
M (F 0 ). The non-classical non-clausal matrix M i/m (F ) of F is the matrix M i/m (F 0 : ε).




                                                     14
Table 4
The (prefixed) non-clausal matrix for classical, intuitionistic and modal logic.

type F pol : p    M (F pol : p)                                      type F pol : p     M (F pol : p)
       0
atom A : p        {{A0 : pa* }}                                      atom A1 : p        {{A1 : pV * }}
α (G ∧ H) : p {{M (G1 : p)}}, {{M (H 1 : p)}}
               1
                                                                     α (¬G)0 : p        M (G1 : pa* )
     (G ∨ H)0 : p {{M (G0 : p)}}, {{M (H 0 : p)}}                         (¬G)1 : p     M (G0 : pV * )
     (G ⇒ H)0 :p {{M (G1 : pa* )}}, {{M (H 0 : pa* )}}               γ    (∀xG)1 : p    M (G[x\x* ]1 : pV * )
β    (G ∧ H)0 : p {{M (G0 : p), M (H 0 : p)}}                             (∃xG)0 : p    M (G[x\x* ]0 : p)
     (G ∨ H)1 : p {{M (G1 : p), M (H 1 : p)}}                        δ    (∀xG)0 : p    M (G[x\t* ]0 : pa* )
     (G ⇒ H)1 :p {{M (G0 : pV * ), M (H 1 : pV * )}}                      (∃xG)1 : p    M (G[x\t* ]1 : p)
ν    (□G)1 : p    M (G1 : pV * )                                     π    (□G)0 : p     M (G0 : pa* )
     (♢G)0 : p    M (G0 : pV * )                                          (♢G)1 : p     M (G1 : pa* )


   A term substitution σT assigns terms to variables. For classical logic, a connection {A01 , A12 }
is σT -complementary iff σT (A1 ) = σT (A2 ). For the non-classical logics, additionally, a prefix
substitution σP assigns strings to prefix variables and is calculated by a prefix unification
that depends on the specific non-classical logic (see also Sections 3.1 and 4.1). For the non-
classical logics, a connection {A01 : p1 , A12 : p2 } is σ-complementary iff σT (A1 ) = σT (A2 ) and
σP (p1 ) = σP (p2 ) for a combined substitution σ = (σT , σP ).
   In the non-clausal connection calculus, the extension rule is generalized to (nested) extension
clauses (e-clauses) and a decomposition rule is added, which splits subgoal clauses [38, 31].

Definition 7 (Non-Clausal Connection Calculus). The non-clausal connection calculus for
classical [38] and non-classical [37] logic is given in Fig. 7 (for classical logic, the underlined
text is to be ignored). A classical non-clausal connection proof for F is a derivation of ε, M, ε
in the non-clausal connection calculus with a term substitution σ = σT , in which all leaves are
axioms. An intuitionistic/modal connection proof for F is a derivation of ε, M i/m (F ), ε with
an admissible (see [20, 37]) combined substitution σ = (σT , σP ), in which all leaves are axioms.


                                                                 C2 , M, {}
    Axiom (A)                                     Start (S)                   and C2 is copy of C1 ∈M
                  {}, M, Path                                     ε, M, ε
                        C, M, Path∪{L2 : p2 }
 Reduction (R)                                             and {L1 :p1 , L2 :p2 } is σ-complementary
                  C∪{L1 : p1 }, M, Path∪{L2 : p2 }
                  C3 , M [C1 \C2 ], Path∪{L1 : p1 }     C, M, Path
  Extension (E)
                                C∪{L1 : p1 }, M, Path
                         and C3 :=β-clauseL2 (C2 ), C2 is copy of C1 , C1 is e-clause of M wrt.
                         Path ∪ {L1 : p1 }, C2 contains L2 : p2 , {L1 :p1 , L2 :p2 } is σ-complementary
                        C ∪ C1 , M, Path
 Decomposition (D)                            and C1 ∈M1
                       C∪{M1 }, M, Path

Figure 7: The non-clausal connection calculus for classical, intuitionistic and modal logic.




                                                      15
Example 7. The (simplified) intuitionistic non-clausal matrix of F4 = ( man(Socrates) ⇒
man(Socrates) ) ∧ ( ( man(Plato) ∧ ∀x(man(x) ⇒ mortal(x)) ) ⇒ mortal(Plato) ) is M4i =
M i (F4 ) = { { {{man(Socrates)0 : a1 V1 }, {man(Socrates)1 : a1 a2 }}, {{man(Plato)1 : a3 V2 },
{man(x)0 : a3 V3 V4 a4 (V3 , x, V4 ), mortal(x)1 : a3 V3 V4 V5 }, {mortal(Plato)0 : a3 a5 }} } } . The gra-
phical non-clausal connection proof for M4i with σ = (σT , σP ) and σT (x) = Plato, σP (V1 ) = a2 ,
σP (V2 ) = a4 (ε, Plato, ε), σP (V3 ) = ε, σJ (V4 ) = ε, σP (V5 ) = a5 is depicted below.

                       man(Socrates)0 :a1 V1       man(Socrates)1 :a1 a2
                                                                                      

                             man(x)0 :a3 V3 V4 a4 (V3 , x, V4 ) 
                                                                                        
         man(Plato)1 :a3 V2                                                      0
                                                                                          
                                             1                     mortal(Plato)   :a  a
                                                                                      3 5
                                  mortal(x) :a3 V3 V4 V5


5.2. nanoCoP
nanoCoP is a compact Prolog implementation of the non-clausal connection calculus for classic
first-order logic (with equality) [31, 36, 35]. It is an extension of the leanCoP code (see Fig. 4).
   In the first step, the input formula F is translated into a non-clausal matrix M = M (F )
according to Table 4 (for intuitionistic and modal logic, prefixes are added to all literals in
the non-clausal matrix M i/m (F )). Every (sub-)clause (I, V, F V ) : C and submatrix J : M
are marked with unique indices I and J, sets V of (free) term and prefix variables that are
newly introduced in C (and sets F V including pairs x : pre(x) of free term variables and their
prefixes, necessary to check if σ is admissible for the non-classical logics). In Prolog, literals
with polarity 1 are marked with “-”. In the second step, for every literal Lit in M the fact
lit(Lit,ClaB,ClaC,Grnd) is asserted into Prolog’s database where ClaC ∈ M is the (largest)
clause in which Lit occurs, ClaB is β-clauseLit (ClaC) [38] and Grnd is g iff the smallest clause
in which Lit occurs is ground (i.e., does not contain variables).
   The source code of the nanoCoP 2.0 core prover is shown in Fig. 8. The underlined code is
necessary only for the non-classical logics and is to be ignored for (classical) nanoCoP.
   The predicate prove(Mat,PathLim,Set,Proof) implements the start rule (lines 1–7) and
iterative deepening (lines 8–12). Mat is the (prefixed) matrix generated in the preprocess-
ing step, PathLim is the size limit for Path, Set is a strategy (see Section 2.3), and Proof
contains the returned (non-clausal) connection proof. The predicate positiveC(Cla,Cla1)
returns the positive clause Cla1 of Cla (implemented in 7 additional lines of code). The predi-
cate prove(Cla,Mat,Path,PathI,PathLim,Lem,PreS,VarS,Set,Proof) implements the
axiom (line 13), the decomposition rule (lines 14–19), the reduction rule (lines 20–23, 27–29,
40–41), and the extension rule (lines 20–23, 31–41) of the calculus in Fig. 7. The substitution
σ is stored implicitly by Prolog. The predicate prove_ec(ClaB,Cla1,Mat,ClaB1,Mat1) calcu-
lates extension clauses (lines 42–52). Additional optimization techniques (see Section 2.3) are
regularity (line 22), lemmata (lines 24–25) and restricted backtracking (line 39).

5.3. nanoCoP-i and nanoCoP-M
nanoCoP-i and nanoCoP-M are compact Prolog implementations of the non-clausal connection
calculus for first-order intuitionistic logic (with equality) and for the first-order modal logics D,
T, S4 and S5 with constant, cumulative and varying domains, respectively [37, 35].




                                                    16
               % start rule
        (1)    prove(Mat,PathLim,Set,[(I^0)^V:Proof]) :-
        (2)        ( member(scut,Set) -> ( append([(I^0)^V^VS:Cla1|_],[!|_],Mat) ;
        (3)            member((I^0)^V^VS:Cla,Mat), positiveC(Cla,Cla1) ) -> true ;
        (4)            ( append(MatC,[!|_],Mat) -> member((I^0)^V^VS:Cla1,MatC) ;
        (5)            member((I^0)^V^VS:Cla,Mat), positiveC(Cla,Cla1) ) ),
        (6)        prove(Cla1,Mat,[],[I^0],PathLim,[],PreS,VarS,Set,Proof),
        (7)        append(VarS,VS,VarS1), domain_cond(VarS1), prefix_unify(PreS).
        (8)    prove(Mat,PathLim,Set,Proof) :-
        (9)        retract(pathlim) ->
       (10)        ( member(comp(PathLim),Set) -> prove(Mat,1,[],Proof) ;
       (11)          PathLim1 is PathLim+1, prove(Mat,PathLim1,Set,Proof) ) ;
       (12)        member(comp(_),Set) -> prove(Mat,1,[],Proof).
               % axiom
       (13)    prove([],_,_,_,_,_,[],[],_,[]).
               % decomposition rule
       (14)    prove([J^K:Mat1|Cla],MI,Path,PI,PathLim,Lem,PreS,VarS,Set,Proof) :-
       (15)        !, member(I^V^FV:Cla1,Mat1),
       (16)        prove(Cla1,MI,Path,[I,J^K|PI],PathLim,Lem,PreS1,VarS1,Set,Proof1),
       (17)        prove(Cla,MI,Path,PI,PathLim,Lem,PreS2,VarS2,Set,Proof2),
       (18)        append(PreS2,PreS1,PreS), append(FV,VarS1,VarS3),
       (19)        append(VarS2,VarS3,VarS), Proof=[J^K:I^V:Proof1|Proof2].
               % reduction and extension rules
       (20)    prove([Lit:Pre|Cla],MI,Path,PI,PathLim,Lem,PreS,VarS,Set,Proof) :-
       (21)        Proof=[Lit:Pre,I^V:[NegLit:PreN|Proof1]|Proof2],
       (22)        \+ (member(LitC,[Lit:Pre|Cla]), member(LitP,Path), LitC==LitP),
       (23)        (-NegLit=Lit;-Lit=NegLit) ->
       (24)           ( member(LitL,Lem), Lit:Pre==LitL, Proof1=[], I=l, V=[],
       (25)              PreS3=[], VarS3=[]
       (26)              ;
       (27)              member(NegL:PreN,Path), unify_with_occurs_check(NegL,NegLit),
       (28)              Proof1=[], I=r, V=[],
       (29)              \+ \+ prefix_unify([Pre=PreN]), PreS3=[Pre=PreN], VarS3=[]
       (30)              ;
       (31)              lit(NegLit:PreN,ClaB,Cla1,Grnd1),
       (32)              ( Grnd1=g -> true ; length(Path,K), K true ;
       (33)                \+ pathlim -> assert(pathlim), fail ),
       (34)              \+ \+ prefix_unify([Pre=PreN]),
       (35)              prove_ec(ClaB,Cla1,MI,PI,I^V^FV:ClaB1,MI1),
       (36)              prove(ClaB1,MI1,[Lit:Pre|Path],[I|PI],PathLim,Lem,PreS1,VarS1,
       (37)                    Set,Proof1), PreS3=[Pre=PreN|PreS1], append(VarS1,FV,VarS3)
       (38)           ),
       (39)           ( member(cut,Set) -> ! ; true ),
       (40)           prove(Cla,MI,Path,PI,PathLim,[Lit:Pre|Lem],PreS2,VarS2,Set,Proof2),
       (41)           append(PreS3,PreS2,PreS), append(VarS2,VarS3,VarS).
               % extension clause (e-clause)
       (42)    prove_ec((I^K)^V:ClaB,IV:Cla,MI,PI,ClaB1,MI1) :-
       (43)        append(MIA,[(I^K1)^V1:Cla1|MIB],MI), length(PI,K),
       (44)        ( ClaB=[J^K:[ClaB2]|_], member(J^K1,PI),
       (45)          unify_with_occurs_check(V,V1), Cla=[_:[Cla2|_]|_],
       (46)          append(ClaD,[J^K1:MI2|ClaE],Cla1),
       (47)          prove_ec(ClaB2,Cla2,MI2,PI,ClaB1,MI3),
       (48)          append(ClaD,[J^K1:MI3|ClaE],Cla3),
       (49)          append(MIA,[(I^K1)^V1:Cla3|MIB],MI1)
       (50)          ;
       (51)          (\+member(I^K1,PI);V\==V1) ->
       (52)          ClaB1=(I^K)^V:ClaB, append(MIA,[IV:Cla|MIB],MI1) ).

Figure 8: The source code of the nanoCoP 2.0, nanoCoP-i 2.0 and nanoCoP-M 2.0 core provers for
classical, intuitionistic and modal logic.




                                                 17
   The source code of nanoCoP-i 2.0 and nanoCoP-M 2.0 is shown in Fig. 8. The underlined text
is added to the nanoCoP code for classical logic. First, nanoCoP-i and nanoCoP-M perform a
classical proof search, in which the prefixes of each connection are stored in PreS. If the search
succeeds, the domain condition is checked using the predicate domain_cond (line 7) and the
prefixes in PreS are unified using the predicate prefix_unify (line 7). These predicates are
implemented by 18 and between 7 to 22 lines of code (depending on the logic), respectively.
   nanoCoP-i 2.0 and nanoCoP-M 2.0 are some of the fastest provers for first-order intuitionistic
logic and first-order modal logic (D, T, S4 and S5), respectively [35].


6. Other CoPs — Re-Implementations and Machine Learning
Several other provers are based on or were inspired by the leanCoP prover. More detailed
information about these provers can be found in the cited references.

6.1. randoCoP, leanCoP-SiNE, leanCoP-Ω and leanCoP on iPod
randoCoP [40] is a theorem prover for classical first-order logic, which integrates randomized
search techniques into the connection prover leanCoP 2.0. By randomly reordering the axioms
of the input problem/formula and the literals within its clausal form, the performance of the
incomplete search strategies of leanCoP 2.0, such as restricted backtracking, can be improved
significantly. A reordering strategy was later also integrated into leanCoP 2.1. At CASC in 2008,
randoCoP 1.1 was among the top three provers that return a proof in the core FOF division.
   leanCoP-SiNE is a theorem prover for classical first-order logic, which integrates the SiNE
preprocessor into leanCoP 2.1. SiNE [41] is an axiom selection system that uses a syntactic
approach based on predicate and function symbols in the input problem/formula to select
axioms that are (likely) relevant to find a proof. It significantly improves performance on very
large problems. At CASC in 2009, leanCoP-SiNE 2.1 ends up in third place in the proof class of
the SUMO reasoning prize.
   leanCoP-Ω is a prover for classical first-order logic with equality and interpreted functions
and predicates for linear integer arithmetic. It combines leanCoP 2.1 with the Omega 1.2 test
system [42]. The prover was developed in cooperation with Holger Trölenberg and Thomas
Raths. At CASC in 2010, leanCoP-Ω 0.1 wins the first (linear integer arithmetic) TFA division.
   leanCoP on iPod [43] is an implementation of leanCoP 2.1 on a (1st-generation) iPod nano.
An iPod nano is a very compact portable media/MP3 player with an 80 MHz ARM 7TDMI 32-bit
CPU and 32 MB of RAM, which was released in 2005. It shows how low leanCoP’s resource
requirements, in particular with respect to RAM are.

6.2. Re-Implementations of leanCoP
Re-implementations and extensions of leanCoP include lolliCoP (implemented in the linear
logic programming language Lolli) [44], fCoP (implemented in OCaml) [45], “C-leanCoP” (imple-
mented in C) [46], RACCOON/leanCoR (for the description logic ALC) [47], fleanCoP/fnanoCoP
(implemented in OCaml) [48], SATCoP (integrating a SAT solver) [49], meanCoP (implemented
in Rust) [50], Connect++ (in C++) [51], and pyCoP/ipyCoP/mpyCoP (in Python) [52].




                                               18
6.3. Machine Learning CoPs
At TABLEAUX 2011, the MaLeCoP [53] prover was presented, one of the first implementations
that integrates Machine Learning (ML) into a theorem prover. It was the starting point for
a whole series of ML provers based on or inspired by leanCoP. Among them are MaLeCoP
(extends leanCoP by integrating ML techniques) [53] FEMaLeCoP (an optimized version of
MaLeCoP) [54], rlCoP (reinforcement learning using Monte Carlo search) [55], plCoP (extending
rlCoP and implemented in Prolog) [56], graphCoP (uses graph neural network models) [57],
monteCoP (using Monte Carlo Tree search) [48], lazyCoP (implements lazy paramodulation
and uses deep neural networks) [58], and FLoP (geared towards finding longer proofs) [59].


7. Conclusion
What started 20 years ago with seven lines of Prolog code, has established itself as a source and
starting point for the development of automated theorem provers for classical and non-classical
logics, as well as for the integration of machine learning into theorem provers. This happened
despite the fact that at the beginning, reception towards leanCoP was controversial and the
author faced some resistance even within his own community. Meanwhile, leanCoP has shown
that compact Prolog implementations are not only more flexible, extendable, “correct” and
easier to maintain than systems with ten thousands lines of low level language code, but they
can have state of the art performance. nanoCoP is perhaps the fastest prover that works on
the original formula structure, combining the advantages of more natural sequent and tableau
provers with the systematic and goal-oriented proof search of connection provers.10
   Perhaps the philosophy behind leanCoP is best summarized by Tony Hoare [60]: “I conclude
that there are two ways of constructing a software design: One way is to make it so simple that
there are obviously no deficiencies and the other way is to make it so complicated that there are
no obvious deficiencies. The first method is far more difficult. It demands the same skill, devotion,
insight, and even inspiration as the discovery of the simple physical laws which underlie the complex
phenomena of nature.”


Acknowledgments
The author would like to thank everyone who contributed directly or indirectly to the develop-
ment of the provers presented in this article, in particular Wolfgang Bibel for his continued,
generous support and (in alphabetical order) Christoph Benzmüller, Michael Färber, Christoph
Kreitz, Thomas Raths, Geoff Sutcliffe, Holger Trölenberg, Josef Urban, Arild Waaler and Lincoln
Wallen. Thanks also go to the anonymous reviewers for their helpful comments.


References
 [1] J. Otten, W. Bibel, leanCoP: lean connection-based theorem proving, Journal of Symbolic
     Computation 36 (2003) 139–161.
10
     The source code of leanCoP and all other provers presented in this paper can be downloaded at www.leancop.de.




                                                         19
 [2] W. Bibel, Matings in matrices, Communications of the ACM 26 (1983) 844–852.
 [3] W. Bibel, Automated Theorem Proving, Artificial intelligence, F. Vieweg und Sohn, 1987.
 [4] B. Beckert, J. Posegga, leanTAP: Lean tableau-based deduction, Journal of Automated
     Reasoning 15 (1995) 339–358.
 [5] R. Letz, G. Stenz, Model elimination and connection tableau procedures, in: A. Robinson,
     A. Voronkov (Eds.), Handbook of Automated Reasoning, Elsevier Science, Amsterdam,
     2001, pp. 2015–2112.
 [6] G. Gentzen, Untersuchungen über das Logische Schließen, Mathematische Zeitschrift 39
     (1935) 176–210, 405–431.
 [7] R. M. Smullyan, First-Order Logic, Ergebnisse der Mathematik und ihrer Grenzgebiete,
     Springer-Verlag, Berlin, Heidelberg, New York, 1971.
 [8] R. Hähnle, Tableaux and related methods, in: A. Robinson, A. Voronkov (Eds.), Handbook
     of Automated Reasoning, Elsevier Science, Amsterdam, 2001, pp. 101–178.
 [9] J. A. Robinson, A machine-oriented logic based on the resolution principle, Journal of
     ACM 12 (1965) 23–41.
[10] W. McCune, L. Wos, Otter – the CADE-13 competition incarnations, Journal of Automated
     Reasoning 18 (1997) 211–220.
[11] J. Urban, MPTP 0.2: Design, implementation, and initial experiments, Journal of Automated
     Reasoning 37 (2006) 21–43.
[12] J. Otten, Restricting backtracking in connection calculi, AI Commun. 23 (2010) 159–182.
[13] J. Otten, leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical
     and intuitionistic logic, in: A. Armando, P. Baumgartner, G. Dowek (Eds.), IJCAR 2008,
     volume 5195 of LNAI, Springer, 2008, pp. 283–291.
[14] M. E. Stickel, A Prolog technology theorem prover: Implementation by an extended Prolog
     compiler, Journal of Automated Reasoning 4 (1988) 353–380.
[15] G. Sutcliffe, The CADE-21 automated theorem proving system competition, AI Commun.
     21 (2008) 71–81.
[16] L. Kovacs, A. Voronkov, First-Order Theorem Proving and Vampire, in: N. Sharygina,
     H. Veith (Eds.), Proceedings of the 25th International Conference on Computer Aided
     Verification, number 8044 in LNAI, Springer, 2013, pp. 1–35.
[17] D. van Dalen, Intuitionistic Logic, John Wiley & Sons, 2017, pp. 224–257.
[18] Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development Coq’Art:
     The Calculus of Inductive Constructions, EATCS Series, Springer, Heidelberg, 2004.
[19] R. L. Constable, et al., Implementing Mathematics with the NuPRL proof development
     system, Prentice–Hall, Englewood Cliffs, NJ, 1986.
[20] L. A. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, Cambridge, 1990.
[21] J. Otten, Clausal connection-based theorem proving in intuitionistic first-order logic, in:
     B. Beckert (Ed.), TABLEAUX 2005, volume 3702 of LNAI, Springer, 2005, pp. 245–261.
[22] A. Waaler, Connections in nonclassical logics, in: A. Robinson, A. Voronkov (Eds.),
     Handbook of Automated Reasoning, Elsevier Science, Amsterdam, 2001, pp. 1487–1578.
[23] R. Statman, Intuitionistic propositional logic is polynomial-space complete, Theoretical
     Computer Science 9 (1979) 67–72.
[24] S. A. Cook, The complexity of theorem-proving procedures, in: Third Annual ACM
     Symposium on Theory of Computing, ACM, New York, 1971, pp. 151–158.




                                              20
[25] P. Blackburn, J. van Bentham, F. Wolter, Handbook of Modal Logic, Elsevier, Amsterdam,
     2006.
[26] M. Fitting, R. L. Mendelsohn, First-Order Modal Logic, Kluwer, Dordrecht, 1998.
[27] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, D. Reidel, Dordrecht, 1983.
[28] J. Otten, Implementing connection calculi for first-order modal logics, in: K. Korovin,
     S. Schulz, E. Ternovska (Eds.), IWIL 2012, volume 22 of EPiC, EasyChair, 2012, pp. 18–32.
[29] J. Otten, MleanCoP: A connection prover for first-order modal logic, in: S. Demri, D. Kapur,
     C. Weidenbach (Eds.), IJCAR 2014, volume 8562 of LNAI, Springer, 2014, pp. 269–276.
[30] K. Gödel, An interpretation of the intuitionistic sentential logic, in: J. Hintikka (Ed.), The
     Philosophy of Mathematics, Oxford University Press, Oxford, 1969, pp. 128–129.
[31] J. Otten, nanoCoP: A non-clausal connection prover, in: N. Olivetti, A. Tiwari (Eds.),
     IJCAR 2016, volume 9706 of LNAI, Springer, 2016, pp. 302–312.
[32] J. Otten, W. Bibel, Advances in connection-based automated theorem proving, in:
     M. Hinchey, J. P. Bowen, E.-R. Olderog (Eds.), Provably Correct Systems, NASA Mono-
     graphs in Systems and Software Engineering, Springer, Cham, 2017, pp. 211–241.
[33] T. Raths, J. Otten, The QMLTP problem library for first-order modal logics, in: B. Gramlich,
     et al. (Eds.), IJCAR 2012, volume 7364 of LNAI, Springer, 2012, pp. 454–461.
[34] C. Benzmüller, J. Otten, T. Raths, Implementing and evaluating provers for first-order modal
     logics, in: L. De Raedt, et al. (Eds.), 20th European Conference on Artificial Intelligence,
     ECAI 2012, IOS Press, Amsterdam, 2012, pp. 163–168.
[35] J. Otten, The nanoCoP 2.0 connection provers for classical, intuitionistic and modal logics,
     in: A. Das, S. Negri (Eds.), TABLEAUX 2021, volume 12842 of LNAI, Springer, 2021, pp.
     236–249.
[36] J. Otten, nanoCoP: Natural non-clausal theorem proving, in: C. Sierra (Ed.), Proceedings
     of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17,
     Sister Conference Best Paper Track, IJCAI, 2017, pp. 4924–4928.
[37] J. Otten, Non-clausal connection calculi for non-classical logics, in: R. Schmidt, C. Nalon
     (Eds.), TABLEAUX 2017, volume 10501 of LNAI, Springer, 2017, pp. 209–227.
[38] J. Otten, A non-clausal connection calculus, in: K. Brünnler, G. Metcalfe (Eds.), TABLEAUX
     2011, volume 6793 of LNAI, Springer, 2011, pp. 226–241.
[39] W. Bibel, J. Otten, From Schütte’s formal systems to modern automated deduction, in:
     R. Kahle, M. Rathjen (Eds.), The Legacy of Kurt Schütte, Springer, Cham, 2020, pp. 217–251.
[40] T. Raths, J. Otten, randoCoP: randomizing the proof search order in the connection
     calculus, in: B. Konev, R. Schmidt, S. Schulz (Eds.), PAAR 2008, volume 373 of CEUR
     Workshop Proceedings, CEUR-WS.org, 2008, pp. 94–102.
[41] K. Hoder, A. Voronkov, Sine qua non for large theory reasoning, in: N. Bjørner, V. Sofronie-
     Stokkermans (Eds.), CADE-23, volume 6803 of LNCS, Springer, 2011, pp. 299–314.
[42] W. Pugh, The omega test: A fast and practical integer programming algorithm for depen-
     dence analysis, Communications of the ACM 31 (1992) 4–13.
[43] J. Otten, The pocket reasoner – automatic reasoning on small devices., in: E. B. Johnsen,
     I. C. Yu (Eds.), Norwegian Informatics Conference, NIK 2018, Open Journal Systems, 2018.
[44] J. S. Hodas, N. Tamura, lolliCoP - A linear logic implementation of a lean connection-
     method theorem prover for first-order classical logic, in: R. Goré, A. Leitsch, T. Nipkow
     (Eds.), IJCAR 2001, volume 2083 of LNCS, Springer, 2001, pp. 670–684.




                                                21
[45] 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
     2015), ACM, 2015, pp. 59–66.
[46] C. Kaliszyk, Efficient low-level connection tableaux, in: H. de Nivelle (Ed.), TABLEAUX
     2015, volume 9323 of LNCS, Springer, 2015, pp. 102–111.
[47] D. M. Filho, F. Freitas, J. Otten, RACCOON: A connection reasoner for the description
     logic ALC, in: T. Eiter, D. Sands (Eds.), LPAR-21, volume 46 of EPiC, EasyChair, 2017, pp.
     200–211.
[48] M. Färber, C. Kaliszyk, J. Urban, Machine learning guidance for connection tableaux,
     Journal of Automated Reasoning 65 (2021) 287–320.
[49] M. Rawson, G. Reger, Eliminating models during model elimination, in: A. Das, S. Negri
     (Eds.), TABLEAUX 2021, volume 12842 of LNCS, Springer, 2021, pp. 250–265.
[50] M. Färber, Connection Provers in Rust, 2022. URL: https://github.com/01mf02/cop-rs.
[51] S. B. Holden, Connect++: A new automated theorem prover based on the connection
     calculus, in: J. Otten, W. Bibel (Eds.), Automated Reasoning with Connection Calculi,
     AReCCa 2023, CEUR Workshop Proceedings, CEUR-WS.org, to appear, pp. 95–106.
[52] F. Rømming, J. Otten, S. B. Holden, Connections: Markov decision processes for classical,
     intuitionistic, and modal connection calculi, in: J. Otten, W. Bibel (Eds.), Automated
     Reasoning with Connection Calculi, AReCCa 2023, CEUR Workshop Proceedings, CEUR-
     WS.org, to appear, pp. 107–118.
[53] J. Urban, J. Vyskocil, P. Stepánek, MaLeCoP machine learning connection prover, in:
     K. Brünnler, G. Metcalfe (Eds.), TABLEAUX 2011, volume 6793 of LNCS, Springer, 2011, pp.
     263–277.
[54] C. Kaliszyk, J. Urban, FEMaLeCoP: Fairly efficient machine learning connection prover,
     in: M. Davis, A. Fehnker, A. McIver, A. Voronkov (Eds.), LPAR-20, volume 9450 of LNAI,
     Springer, 2015, pp. 88–96.
[55] C. Kaliszyk, J. Urban, H. Michalewski, M. Olšák, Reinforcement Learning of Theorem
     Proving, in: Advances in Neural Information Processing Systems, volume 31, Curran
     Associates, Inc., 2018.
[56] Z. Zombori, J. Urban, C. E. Brown, Prolog technology reinforcement learning prover, in:
     N. Peltier, V. Sofronie-Stokkermans (Eds.), IJCAR 2020, volume 12167 of LNAI, Springer,
     2020, pp. 489–507.
[57] M. Olšák, C. Kaliszyk, J. Urban, Property invariant embedding for automated reasoning,
     in: G. D. Giacomo, et al. (Eds.), ECAI 2020, volume 325 of Frontiers in Artificial Intelligence
     and Applications, IOS Press, Amsterdam, 2020, pp. 1395–1402.
[58] M. Rawson, G. Reger, lazyCoP: Lazy Paramodulation Meets Neurally Guided Search,
     in: A. Das, S. Negri (Eds.), TABLEAUX 2021, volume 12842 of LNAI, Springer, 2021, pp.
     187–199.
[59] Z. Zombori, A. Csiszárik, H. Michalewski, C. Kaliszyk, J. Urban, Towards finding longer
     proofs, in: A. Das, S. Negri (Eds.), TABLEAUX 2021, volume 12842 of LNCS, Springer, 2021,
     pp. 167–186.
[60] C. A. R. Hoare, The emperor’s old clothes, Communications of the ACM 24 (1981) 75–83.




                                                22