Automated proof search with connection tableaux, such as implemented by Otten's leanCoP prover, depends on backtracking for completeness. Otten's restricted backtracking strategy loses completeness, yet for many problems, it significantly reduces the time required to find a proof. I introduce a new, less restricted backtracking strategy based on the notion of exclusive cuts. I implement the strategy in a new prover called meanCoP and show that it greatly improves upon the previous best strategy in leanCoP.
Bibel’s connection method [
One of the most influential connection provers is Otten’s leanCoP [
This article studies backtracking that guides connection proof search. In particular, a backtracking strategy deals with the question: When a literal L is solved with a proof P , which alternative proofs P ′ to solve L can proof search consider afterwards? A complete backtracking strategy does not impose any restriction on P ′; that is, it allows proof search to consider all different proofs P ′ for L. Otten showed that by restricting backtracking, the prover becomes significantly more effective for many problems as this reduces the search space, at the expense of losing completeness (section 3). His “restricted backtracking” strategy prevents exploring any alternative proof P ′ for a solved literal L. In this paper, I introduce a novel incomplete strategy called “less restricted backtracking”, which prevents exploring any alternative proof P ′ for a
solved literal L where P ′ starts with the same root step as P (section 4). In other words, for any literal L, unrestricted backtracking considers all proofs, restricted backtracking considers only a single proof, and less restricted backtracking considers only proofs with differing root steps.
I unexpectedly discovered less restricted backtracking upon implementing a new prover called meanCoP based on leanCoP (section 5). The new strategy improves upon the former best strategy in leanCoP dramatically (section 6).
In this article, we will use classical first-order logic without equality. However, the techniques shown can be also applied to non-classical logics.
A term t is either a variable (denoted by x, y, z) or the application of a constant (denoted by a, b, c) to terms. An atom A is the application of a predicate (denoted by p, q, r) to terms. Predicates and constants have associated fixed arities. A literal L is an atom A or its negation ¬A. The complement of a literal is defined such that A = ¬A and ¬A = A. A term substitution σ is a mapping from variables to terms. Applying a substitution σ to a literal L, denoted as σL, substitutes all variables of L with their mappings. Two literals L1, L2 can be unified under a substitution σ if σL1 = σL2.
A formula in conjunctive normal form (CNF) is a conjunction (∧) of disjunctions (∨) of literals. A clause is a set of literals, and a matrix is a set of clauses. We interpret a clause as the disjunction of its literals, and we interpret a matrix as the conjunction of its (interpreted) clauses. It is easy to see that for each formula in CNF, there is an equivalent matrix.
(p(x) ∨ q(x)) ∧ (¬p(y) ∨ r(y)) ∧ ¬p(z) ∧ ¬r(a) ∧ ¬r(b) ∧ ¬q(c).
M = ""p(x)#"¬p(y)#h¬p(z)ih¬r(a)ih¬r(b)ih¬q(c)i , # q(x) r(y) which we will use as running example throughout this paper.
In this paper, we treat proof search using the clausal connection tableaux calculus [
S where C2 is a copy of C1 ∈ M
C, M, P ath ∪ {L′} C ∪ {L}, M, P ath ∪ {L′} R where σ(L) = σ(L′) C2 \ {L′}, M, P ath ∪ {L} C, M, P ath
C ∪ {L}, M, P ath where C2 is a copy of C1 ∈ M and L′ ∈ C2 with σ(L) = σ(L′)
E
An application of a proof rule is called a proof step. A derivation for ⟨C, M, P ath⟩ with the term substitution σ, in which all leaves are axioms, is called a connection proof for ⟨C, M, P ath⟩. A connection proof for ⟨ε, M, ε⟩ is called a connection proof for M .
Bibel proved soundness and completeness of the calculus: for any formula F in CNF, we have
that F is unsatisfiable iff there is a connection proof for the matrix corresponding to F [
Proof search proceeds by constructing derivations from bottom to top. We can understand a derivation for ⟨C, M, P ath⟩ as an attempt to prove (M ∧ P ath) =⇒ C, where we interpret P ath as conjunction of its literals. By interpreting ε as empty set, a derivation for ⟨ε, M, ε⟩ can be seen as a proof attempt of M =⇒ ⊥.
We say that any reduction or extension step as in Figure 1 connects L to L′. We illustrate this by drawing an arrow from L to L′ in the matrix. In this paper, we will only use extension steps in examples.
Let us walk through a failed proof search attempt for the matrix M from Example 1, and show its graphical representation as well as its resulting derivation in the calculus. 2 {}, M, {p(x), r(y)}
{}, M, {p(x)} {r(y)}, M, {p(x)} E (1.2) · · · · {q(x)}, M, {}
E (1.1) {p(x), q(x)}, M, {} ε, M, ε
S
Example 2. Consider matrix M from Example 1. Matrix (1) of Figure 2 illustrates a proof search attempt through M . We write the proof step n in matrix m as (m.n) and mark situations in which we are stuck with . The proof search proceeds as follows: We first choose the first clause in M as start clause. This obliges us to connect both p(x) and q(x). We start with p(x), which we choose to connect in step (1.1) to ¬p(y), setting σ(x) = y. This in turn obliges us to connect r(y), which we choose to connect in step (1.2) to ¬r(a), setting σ(x) = σ(y) = a. We are now left with the obligation to connect q(x). However, at this point (1.3), we cannot connect q(x) to any literal due to σ. As we are stuck at this point, we mark this with . Figure 3 shows a derivation for M that corresponds to that proof search. The extension steps in the derivation are labelled like the corresponding proof steps in matrix (1). The derivation is not a connection proof for M , because the leaf ⟨{q(x)} , M, {}⟩ is not an axiom.
This example illustrates that search in connection tableaux is not confluent, i.e., we can end up with unprovable leaves in derivations for a matrix M although the formula corresponding to M is unsatisfiable. This makes it necessary to backtrack to previous states of derivations to obtain a complete proof search method. We will study two backtracking strategies in the next section.
In the failed proof attempt shown in Example 2, we frequently talked about obligations and choices. Fulfilling obligations assures soundness, and making alternative choices exhaustively assures completeness.
Otten’s unrestricted backtracking strategy [
Example 3 (Unrestricted Backtracking). Consider the proof search attempt in Example 2. The last choice we made in that example was to connect r(y) to ¬r(a) as part of step (1.2). We can make a different choice here, namely connect r(y) to ¬r(b), which we perform in step (2.1). However, as it turns out, this will not help us once we have to deal with q(x) anew in step (2.2), for now we have σ(x) = σ(y) = b, which still does not permit a connection from q(x). So we backtrack again, leading to the proof search shown in matrix (3). This time, the last choice was to connect r(y) to ¬r(b), but now, we cannot find a different way to connect r(y). So we look at our second to last choice, namely to connect p(x) to ¬p(y). We can make an alternative choice here as step (3.1), namely to connect p(x) to ¬p(z). Now we are back once more to the dreaded q(x), but finally, due to σ(x) = σ(z) not pointing to an actual term, we can connect q(x) to ¬q(c) as step (3.2). This concludes the proof, as we have no more obligations left at this point.
Otten’s restricted backtracking strategy [
Definition 2 (Principal literal, solved literal). When the reduction or extension rules are applied, the literal L (see Figure 1) is called the principal literal of the proof step. A reduction step solves a literal L iff L is its principal literal. An extension step S solves a literal L iff L is the principal literal of S and there is a proof for the left premise of S, i.e., there is a derivation for the left premise of S having only axioms as leaves.
The restricted backtracking strategy works like the unrestricted one, with one exception: Once a literal is solved, restricted backtracking discards all choices to solve the literal differently. Example 4 (Restricted Backtracking). Consider matrix (1) of Figure 2. Proof step (1.1) does not solve any literal, so at this point, proof search behaves like in Example 3. Proof step (1.2) solves r(y), so at that point, alternative choices to solve r(y) are discarded. At the same time, step (1.2) also solves p(x), so alternative choices to solve p(x) are discarded as well. In proof step (1.3), we note that q(x) cannot be connected. However, unlike in Example 3, we have no alternative choices left to backtrack to because they were discarded as a result of step (1.2). That means that the restricted backtracking strategy cannot find a proof once we commit to connecting p(x) to ¬p(y) as first step.
Restricted backtracking can be decomposed into two cuts: cuts on reduction and cuts on extension steps. Kaliszyk already implemented these two cuts separately, but did not describe it, as they are usually most useful in conjunction. Here, the distinction arises naturally, as it allows to more succinctly describe a new backtracking strategy.
I will now distinguish inclusive and exclusive cuts. An inclusive cut discards all alternatives to solve a literal, whereas an exclusive cut discards all alternatives to solve a literal, except for derivations starting with a different proof step. Otten’s restricted backtracking strategy shown in section 3 uses inclusive cuts on both reduction and extension steps. To the best of my knowledge, exclusive cuts have not been researched before.
Example 5 (Exclusive Cut). We will, for the last time, revisit the proof search in Figure 2. After proof step (1.2), exclusive cut discards alternative ways to solve p(x), except for derivations starting with different extension steps. As a result, after being stuck at step (1.3) with q(x), we can backtrack unlike in Example 4, namely to the proof search in matrix (3), because it solves p(x) in step (3.1) starting with a different extension step. From there, proof search behaves again like in Example 3, solving the problem in step (3.2) after connecting q(x).
To sum up the outcomes of different backtracking strategies on the proof search in Figure 2: The complete strategy (Example 3) solves the problem, going through all stages from (1) to (3). (a) Reduction (R).
(b) Extension, inclusive (EI).
(c) Extension, exclusive (EX).
The exclusive cut (Example 5) also solves the problem, but takes one stage less, going through only (1) and (3). The inclusive cut (Example 4) fails after (1). For this example, exclusive cut therefore is the most efficient strategy.
For reduction steps, an exclusive cut is equivalent to no cut, so I distinguish between inclusive and exclusive cut only for extension steps. I abbreviate (inclusive) cut on reduction steps as R and inclusive and exclusive cut on extension steps as EI and EX, respectively. Otten’s restricted backtracking strategy can be described as a combination of R and EI, written as REI.
Figure 4 visualises the alternatives that are cut once a literal is solved. In each of the trees, the left child of the root is a proof step S that solves a literal, the children of the left child are alternatives to proof steps that are descendants of S, and the right child is the alternative to S. Reduction and extension steps are marked as R and E, respectively, and alternatives are marked as “?”. Both the R and EI cut are inclusive cuts because the right child is cut, and the EX cut is exclusive because the right child is preserved. Both EI and EX cuts eliminate all alternatives below the proof step.
The seemingly small difference between inclusive and exclusive cut has a large impact on the effectiveness of the prover. We will see this in the evaluation (section 6).
The connection prover leanCoP is compactly implemented in Prolog as a recursive predicate
prove that takes C and P ath as parameters, using a helper predicate lit that models M [
Based on Kaliszyk’s stack-based implementation, I implemented a connection prover called
meanCoP in Rust.2 Like C++, Rust favours zero-overhead abstractions [
a1 (a) No cut.
(b) Exclusive.
(c) Inclusive. contains a tiny proof checker that is run before outputting a proof. This is useful to assure that the prover is sound.
meanCoP supports most major features of leanCoP, such as conjecture-directed search,
regularity, and lemmas [
Kaliszyk uses a stack of alternatives to keep track of proof steps to backtrack to. This allows for a compact implementation of inclusive and exclusive cuts. Figure 5 shows the effect of inclusive and exclusive cut on the stack of alternatives. Figure 5a shows the initial situation of the stack after a literal was solved with a proof step whose alternative is an. Above an are alternatives to proof steps added after an, and below an are alternatives to proof steps added before an. Using no cut does not change the stack at this point. Both exclusive and inclusive cut eliminate all alternatives added after an, but the exclusive cut (Figure 5b) keeps one alternative more than the inclusive cut (Figure 5c), namely an. Using inclusive instead of exclusive cut amounts to truncating the stack of alternatives to length n instead of length n − 1 once a literal was solved.
I evaluate the performance of meanCoP (section 5) and other provers on several first-order
problem datasets.3 For every dataset and prover, I measure the number of problems solved
by the prover in a given time. All evaluated connection provers use a single strategy with
conjecture-directed search and non-definitional (i.e. standard or naive) translation into CNF
[
I use a 48-core server with AMD Opteron 6174 2.2GHz CPUs, 320 GB RAM, and 0.5 MB L2 cache per CPU. Each problem is always assigned one CPU. I run every prover with a timeout of 10 seconds per problem.
I use several first-order logic datasets for evaluation, with statistics given in Table 1:
• TPTP [
It comes in the two flavours “bushy” and “chainy”: In the “chainy” dataset, every problem
contains all facts stated before the problem, whereas in the “bushy” dataset, every problem
contains only the Mizar premises required to prove the problem.
• Miz40 contains the problems from the Mizar library for which at least one ATP proof has
been found using one of the 14 combinations of provers and premise selection methods
considered in [
Flyspeck project, which finished in 2014 a formal proof of the Kepler conjecture [
Table 2 shows the number of problems solved by strategy. For all datasets, the complete strategy without any cut solves the least problems. Among the previously implemented cuts, namely R, EI, and REI, REI solves the most problems, except on the dataset FS-top, where R prevails. Adding cut on reduction (R) to any strategy increases the number of solved problems, except for the Miz40 dataset. The strategies with exclusive cut on extension steps (EX, REX) outperform those with inclusive cut (EI, REI) on all datasets except for the chainy one. I explore the reason for this in subsection 6.2.
On most datasets, the strategies using exclusive cut bring an impressive improvement of the prover power. The REX strategy increases the number of solved problems compared to the REI strategy by 16.4% for bushy, 17.0% for FS-top (12.3% if we compare with the R cut), and 19.0% for Miz40. Remarkably, on TPTP, the improvement turns out much smaller with only 6.9%.
Table 3 shows the union of problems solved by a portfolio of strategies. The first row shows the problems solved by any of the four previously used cut strategies, including the unrestricted backtracking strategy without cut, but also combinations of cut on reduction and inclusive cut on extension, while excluding our new exclusive cut. Comparing the first row with the REX results from Table 2, we see that the new REX strategy solves single-handedly more problems than a union of four strategies on the bushy and Miz40 datasets, which is quite noteworthy. The second row shows the problems solved by any of the two most powerful strategies, including the REX strategy that uses exclusive cut. This combination is better than the combination of all previous cut strategies in the first row on all datasets except for chainy, where it is only two problems behind. Combining all strategies (row 3) clearly boosts the number of solved problems compared to the previously available strategies (row 1), namely 11.2% for bushy, 4.8% for TPTP, 9.8% for Miz40, and 7.2% for FS-top.
In conclusion, the new strategies do not only prove more problems, but the problems they solve are also sufficiently complementary from the problems solved by previously available strategies. This makes the new strategies attractive in portfolio modes. 6.2. Proof analysis I compare the proofs of the complete, REX, and REI strategies, similar to Otten’s comparison of the complete and REI strategies [10, sec. 4.2].
There are two indicators for the quality of a cut strategy C2 with respect to a more complete cut strategy C1: which percentage of C1 proofs C2 finds, and how many more inferences C1 takes to find these proofs. When two problems are solved identically by C2 and C1, the additional backtracking done by C1 is superfluous for the proof. The fewer inferences C2 takes to find identical proofs, the more likely it is that C2 also finds proofs which are out of reach for C1 in a given time limit.
Table 4 shows the number of problems for which two strategies find identical proofs. To understand how these numbers emerge, let us consider the chainy dataset, comparing the complete (C1 = None) and the REX (C2 = REX) strategies. Here, Table 2 shows us that C1 solves 208 and C2 solves 294 chainy problems. C2 finds for 186 of the 208 problems solved by C1 the same proof as C1, which amounts to the 89.4% given in Table 4. Note that C2 solves 203 of the 208 problems that C1 solves, which means that for 17 problems, it finds different proofs than C1.
Of all proofs found by the complete strategy, REX finds between 89.4% (chainy) to 66.5% (bushy), whereas REI finds only between 68.3% (TPTP) and 46.7% (bushy). REI also finds only between 66.6% (FS-top) and 40.8% (bushy) of the proofs found by REX. This shows that there are significantly fewer proofs requiring unrestricted backtracking (no cut) than proofs requiring backtracking that replaces root steps (REX).
We are now going to analyse how much different strategies reduce the search space. For this, we will compare the number of inferences taken by two strategies when they find the same proofs. Given two strategies C1 and C2, we can construct an I as follows: if C1 and C2 found the same proof p for a problem, then (p, n1, n2) ∈ I, where n1 and n2 are the number of inferences taken by C1 and C2. Table 5 shows the ratio of the sum of all inferences, calculated by
P(p,n1,n2)∈I n1 , P(p,n1,n2)∈I n2 and Table 6 shows the average of the ratios of inferences, calculated by
X (p,n1,n2)∈I n2 n1 ÷ |I|.
In both cases, the higher a value, the more C2 reduces the search space with respect to C1.
Let us look at Table 5. For example, on the Miz40 dataset, for all problems identically solved by REX and the complete strategy, the sum of inferences by the complete strategy is 37.4 times the sum of inferences by the REX strategy. This is the highest ratio for REX with respect to the complete strategy. REX also achieves on Miz40 the largest increase of solved problems compared to the complete strategy (+74.5%). Conversely, on TPTP, where REX shows the smallest inference ratio (4.4), REX also least improves the number of solved problems (+22.8%). On most datasets, the ratios between REI and REX are significantly smaller than the ratios between REX/REI and the complete strategy; for example, on the Miz40 dataset, REI reduces inferences compared to REX only by 2.4, whereas REX and REI reduce inferences compared to the complete strategy by 37.4 and 54.6. This indicates that REX and REI are much “closer” to each other than to the complete strategy. Notable exceptions are the chainy and TPTP datasets, where the ratios between the complete strategy and REX are quite similar to the ratios between REX and REI.4 Interestingly, these are the datasets where REX proves fewer (chainy) or only few more (TPTP) problems than REI. On datasets like chainy that contain many problems with unusually many axioms, implying a larger explosion of the search space, a more aggressive cut such as REI turns out to be beneficial. In general, we can observe that REX yields the best results when REX greatly reduces the search space with respect to the complete strategy and REI slightly reduces the search space with respect to REX.
In summary, REX is successful because it conserves a considerable amount of existing proofs,
while sufficiently reducing the number of inferences in order to find new proofs.
6.3. Comparison with other leanCoP implementations
I evaluate meanCoP and two other implementations of leanCoP, namely leanCoP 2.1 using the
Prolog compiler ECLiPSe 5.10, and fleanCoP, which is a reimplementation of leanCoP in OCaml
using streams [
Table 7 shows the runtime of different leanCoP implementations on sets of problems solved by the original leanCoP. The meanCoP prover is between 27.7 (FS-top) and 6.5 (TPTP) times faster than the original leanCoP and between 11.1 (Miz40) and 2.4 (TPTP) times faster than its OCaml reimplementation using streams.
Table 8 shows that the higher performance of meanCoP translates to a vastly increased
number of proven problems. The largest improvement can be seen on the chainy dataset, where
4This can be also seen in Table 6, where the ratio between REX and REI on TPTP is unusually high and clearly
exceeds the ratio between REX and the complete strategy.
5This amounts to running meanCoP with --conj --cuts rei, leanCoP with SET='[nodef,conj,cut]', and
fleanCoP with -schedule 0 -nodefcnf.
leanCoP, fleanCoP and meanCoP (all using the REI strategy) prove 182, 289 (+58.8%), and 341
(+87.4% compared to leanCoP and +18.0% compared to fleanCoP) problems, respectively.
6.4. Comparison with other provers
I compare meanCoP with several non-connection provers that I previously evaluated in joint
work with Kaliszyk and Urban [14, table 2]. In particular, I evaluate Vampire 4.0 [
I also evaluate two versions of leanCoP 2.1: First, I evaluate leanCoP 2.1 with strategy scheduling, which will be simply called “leanCoP” in this section. Running leanCoP with a timeout of 10 seconds runs about 10 different search strategies for one second each. Second, I evaluate the first strategy in the strategy schedule of leanCoP 2.1 which searches using restricted backtracking until a path limit of 7, then switches to a complete search with unrestricted backtracking. I call this strategy “leanCoP-CC7”. Unlike all other evaluated connection provers with a single strategy, leanCoP-CC7 does not use conjecture-directed search; furthermore, it uses definitional translation into CNF for the conjecture of the input problem. Finally, I evaluate an adapted version of leanCoP-CC7 with conjecture-directed search and with non-definitional translation into CNF. I call this strategy “leanCoP-NCCC7”.6 6leanCoP-CC7 and leanCoP-NCCC7 amount to running leanCoP with SET='[cut,comp(7)]' and SET='[nodef,conj,cut,comp(7)]', respectively.
Table 9 shows the results: Vampire proves most problems on all datasets except for FS-top, where E prevails. On the chainy dataset, meanCoP proves more problems than E, which is likely due to the conjecture-directed search. Metis proves the fewest problems, except on the Miz40 dataset, where it proves more problems than any connection prover, but less than Vampire and E. leanCoP-CC7 proves more problems than Metis on all datasets except for Miz40, but proves fewer problems than leanCoP (with strategy scheduling) on all datasets. meanCoP-REI proves more problems than leanCoP on all datasets but Miz40 and FS-top, and meanCoP-REX proves more problems than leanCoP on all datasets.
Table 10 shows for several provers P how many problems meanCoP-REX can solve that were not solved by P . For example, it shows that meanCoP-REX proves 1038 FS-top problems that were not solved by Vampire, which solves 6358 problems in total. The last line in Table 10 shows the number of problems that meanCoP-REX solves which no other prover in the table solves.
Figure 6 shows for several provers the number of problems on the bushy dataset proved up to a certain time. meanCoP-REX proves considerably more problems than Vampire in the first 10 milliseconds, namely 428 versus a single one. However, Vampire catches up after about 50 milliseconds, leaving all other provers behind. leanCoP and leanCoP-REI solve their first problem about 50 milliseconds after any other prover, which is due to the relatively high start-up time caused by the compilation of the prover at each run. After 50 milliseconds, the order between the provers remains stable. The curves for the provers without strategy scheduling (leanCoP-REI, meanCoP-REI, meanCoP-REX) flatten with time, whereas the curves for Vampire
Vampire meanCoP-REX meanCoP-REI
leanCoP leanCoP-REI 0 2 4 Time [s] 6 8 10 and leanCoP shows several “bumps” due to strategy scheduling. The average time used to solve a problem is 0.53 seconds for meanCoP-REI, 0.64 seconds for meanCoP-REX, 0.76 seconds for leanCoP-REI, 0.87 seconds for leanCoP, and 0.99 seconds for Vampire.
The MaLeCoP prover by Urban et al. [
Other connection provers have moved away more from leanCoP’s traditional
backtrackingbased search. I developed monteCoP in joint work with Kaliszyk and Urban [
We evaluate FEMaLeCoP and monteCoP on the bushy dataset, using 60 seconds timeout, definitional clausification and the REI strategy. Comparing the non-learning with the learning versions of the provers, the increase in number of solved problems is from 563 to 601 for monteCoP (+6.7%) and from 577 to 592 for FEMaLeCoP (+2.6%) [14, table 8], thus far below the increase of 16.4% gained in the current work.
Kaliszyk et al. evaluate rlCoP on the Miz40 dataset, where it proves 16108 problems after 10 iterations of training. Although I evaluate meanCoP on the same dataset, where meanCoP proves 16134 problems, it is unfortunately difficult to compare the results for two reasons: First, Kaliszyk et al. limit the number of inferences instead of the time allotted to the prover. Second, most inferences performed by rlCoP end up in prover states that are not actually explored, due to not being chosen by Monte Carlo Tree Search.
Another line of work extends connection provers with native support for equality. Rawson’s
lazyCoP is a connection prover based on Paskevich’s connection tableaux calculus with lazy
paramodulation [
Otten’s ileanCoP for intuitionistic logic [
I introduced a new kind of cut on extension steps called exclusive cut, which discards all alternatives to solve a literal, except for derivations starting with a different extension step. I implemented the described techniques in a new prover called meanCoP. Evaluating meanCoP on several first-order problem datasets yielded that a combination of cut on reduction steps and exclusive cut on extension steps (REX) improves the number of solved problems compared to the previous best strategy by up to 19%.
Acknowledgements I am grateful to the anonymous CADE, TABLEAUX, and AReCCa reviewers as well as to Jasmin Blanchette, Mathias Fleury, Cezary Kaliszyk, and Petar Vukmirović for their comments on drafts of this paper. This work has been supported by the Schrödinger grant (J 4386) of the Austrian Science Fund (FWF).