The paper presents several proof search optimization techniques for non-clausal connection calculi. These techniques are implemented and integrated into the non-clausal connection prover nanoCoP. Their effectiveness is evaluated on the problems in the TPTP library. Together with a fixed strategy scheduling, these techniques are the basis of the new version 1.1 of nanoCoP.
Most of the popular efficient proof search calculi require the input formula to be in
clausal form, i.e. in disjunctive or conjunctive normal form. First-order formulae that
are not in clausal form are translated into clausal form in a preprocessing step. While
the use of a clausal form technically simplifies the proof search and the required data
structures, it also has some disadvantages. Even the definitional translation into clausal
form introduces a significant overhead into the proof search [
Non-clausal connection calculi for classical logic [
This paper presents techniques for optimizing the proof search in non-clausal
connection calculi (Section 3) and shows how these can be implemented and integrated
into the (classical) nanoCoP prover (Section 4). Among these techniques are restricted
backtracking and clause reordering techniques, which are already successfully used in
clausal connection calculi [
A (first-order) formula (denoted by F) is built up from atomic formulae, the connectives
:, ^, _, ), and the standard first-order quantifiers 8 and 9. An atomic formula (denoted
by A) is built up from predicate symbols and terms. A literal L has the form A or :A.
Its complement L is A if L is of the form :A; otherwise L is :L. A connection is a
set fA; :Ag of literals with the same predicate symbol but different polarities. A term
substitution s assigns terms to variables. The non-clausal connection calculus uses
nonclausal matrices. A non-clausal matrix M of a formula F is a set of clauses, in which
each clause consists of literals and (sub)matrices, and can be seen as a representation of
a formula in negation normal form; see [
The axiom and the rules of the non-clausal connection calculus are given in
Figure 1. Compared to the formal clausal connection calculus [
For example, the formula P(a)^(8y(P(y))P(g(y)))_ :(Q)Q)) ) P(g(g(a))) has the non-clausal matrix (the polarity 1 is used to represent negation):
ffP(a)1g; fffP(y)0; P(g(y))1gg; ffQ1g; fQ0ggg; fP(g(g(a)))0gg which has the following graphical representation and connection proof (using the term substitution s with s (y) = a and s (y0) = g(a)): 2
2 66 P(a)1 66 4 4
P(y)0 P(g(y))1
copy z P(y}0|)0
P(g(y0))1 Q1
Q0 { 3
3 77 P(g(g(a)))0 77 . 5 5
fg; M; Path
C2; M; fg e; M; e and s (L1)=s (L2)
and C2 is copy of C12M and C3:=b -clauseL2 (C2), C2 C; M; Path is copy of C1, C1 is e-clause of M wrt. Path [ fL1g, C2 contains L2 with s (L1) = s (L2) C [C1; M; Path
and C12M1
The following proof search optimization techniques are integrated into the non-clausal connection calculus: regularity, lemmata, restricted backtracking, positive and conjecture start clauses, reordering clauses, and strategy scheduling. 3.1
Regularity and Lemmata
Regularity is an effective technique for pruning the search space in clausal connection
calculi [
8 L0 2 C [fL1g : s (L0) 62 s (Path) .
Additional backtracking is avoided if the term substitution s is not modified in order to satisfy the regularity condition, e.g., by applying the restriction only to ground literals.
The idea of lemmata is to reuse subproofs during the proof search [
Restricted Backtracking As proof search in the presented connection calculus is not confluent, backtracking is necessary in order to achieve completeness. In the clausal connection calculus backtracking is necessary when choosing clause C1 in the extension rule or literal L1 in the reduction or extension rule. In the non-clausal calculus (see Figure 1) additional backtracking is required when choosing C1 in the decomposition rule (but no backtracking is required when choosing M1).
The idea of restricted backtracking is to cut off any alternative solutions/connections
once a literal from the subgoal clause has been solved [
Positive and Conjecture Start Clauses By default, the selection of the start clause C1 in the start rule (see Figure 1) is restricted to positive clauses. A clause is positive iff all of its elements (matrices and literals) are positive; a matrix is positive iff it contains at least one positive clause; a literal is positive iff its polarity is 0. Furthermore, clauses that are not positive can be deleted from the start clause C1 (or its copy C2). 1 Observe that the restriction to the active path is necessary in the non-clausal case as completeness is lost, otherwise; see, e.g., the valid matrix ffp0g; fp1; ffp0g; fq0ggg; fq1gg .
Whereas selecting positive start clauses can significantly prune the search space, this technique is less appropriate for problems with a large number of axioms, i.e. formulae of the form A1 ^ ::: ^ An ) C for a “large” n. In this case it is more goal-oriented to start with clauses of the conjecture C, which leads to a smaller search space.2 3.4
Reordering Clauses As already mentioned in Section 3.2, the connection calculus is not proof confluent. The order in which clauses and literals are selected if more than one connection is possible has a significant impact on the proof search. This is even more important for incomplete techniques, such as restricted backtracking. One clause order might lead to an incomplete proof search, while another one might quickly lead to a proof. Hence, reordering clauses is a crucial technique for connection calculi using restricted backtracking. For non-clausal calculi it is important that a reordering technique leads to diverse orders even for small sets of clauses, e.g., if a (sub)matrix contains only two or three clauses. 3.5
Strategy Scheduling Trying different techniques or methods when solving a hard problem is, in general, a successful approach. Hence, when trying to prove a formula, a mix of different techniques or strategies is more likely to be successful. A strategy scheduling would subsequently try different techniques to find a proof of a formula, e.g., positive and conjecture start clauses, with and without restricted backtracking, or using different clause orders.
The proof search optimization techniques described in Section 3 have been implemented and integrated into the non-clausal connection prover nanoCoP, which is available under the GNU General Public License and can be downloaded from the following website: http://www.leancop.de/nanocop/ .
In a first step the input formula F is translated into a non-clausal (indexed) matrix
M; in the second step this matrix is written into Prolog’s database using the literal
lit(Lit,ClaB,ClaC,Grnd); see [
The source code of the nanoCoP core prover is shown in Figure 2. The predicate prove(Mat,PathLim,Set,Proof) implements the start rule (lines 1–11). Mat is the matrix generated in the preprocessing step, PathLim is the maximum size of the active path used for iterative deepening (lines 7–11), Set is a strategy (see below), and Proof contains the returned connection proof.
The predicate prove(Cla,Mat,Path,PathI,PathLim,Lem,Set,Proof) implements the axiom (line 12), the decomposition rule (lines 13–17), the reduction rule (lines 18– 21, 24–25, 34), and the extension rule (lines 18–21, 27–45) of the non-clausal connection calculus in Figure 1. It succeeds iff there is a connection proof for the tuple “Cla, Mat, Path” with jPathj < PathLim. The predicate prove_ec calculates an appropriate extension clause (lines 35–45). The substitution s is stored implicitly by Prolog. 2 This approach is incomplete, though, as shown by the following formula: (P ^ :P) ) Q . % start rule prove(Mat,PathLim,Set,[(I^0)^V:Cla1|Proof]) :( member(scut,Set) -> ( append([(I^0)^V:Cla1|_],[!|_],Mat) ; member((I^0)^V:Cla,Mat), positiveC(Cla,Cla1) ) -> true ; ( append(MatC,[!|_],Mat) -> member((I^0)^V:Cla1,MatC) ; member((I^0)^V:Cla,Mat), positiveC(Cla,Cla1) ) ), prove(Cla1,Mat,[],[I^0],PathLim,[],Set,Proof). prove(Mat,PathLim,Set,Proof) :retract(pathlim) -> ( member(comp(PathLim),Set) -> prove(Mat,1,[],Proof) ;
PathLim1 is PathLim+1, prove(Mat,PathLim1,Set,Proof) ) ; member(comp(_),Set) -> prove(Mat,1,[],Proof). % axiom prove([],_,_,_,_,_,_,[]). % decomposition rule prove([J:Mat1|Cla],MI,Path,PI,PathLim,Lem,Set,Proof) :- !, member(I^_:Cla1,Mat1), prove(Cla1,MI,Path,[I,J|PI],PathLim,Lem,Set,Proof1), prove(Cla,MI,Path,PI,PathLim,Lem,Set,Proof2), append(Proof1,Proof2,Proof). % reduction and extension rules prove([Lit|Cla],MI,Path,PI,PathLim,Lem,Set,Proof) :
Proof=[[I^V:[NegLit|ClaB1]|Proof1]|Proof2], \+ (member(LitC,[Lit|Cla]), member(LitP,Path), LitC==LitP), (-NegLit=Lit;-Lit=NegLit) -> ( member(LitL,Lem), Lit==LitL, ClaB1=[], Proof1=[] ; member(NegL,Path), unify_with_occurs_check(NegL,NegLit), ClaB1=[], Proof1=[] ; lit(NegLit,ClaB,Cla1,Grnd1), ( Grnd1=g -> true ; length(Path,K), K<PathLim -> true ;
\+ pathlim -> assert(pathlim), fail ), prove_ec(ClaB,Cla1,MI,PI,I^V:ClaB1,MI1), prove(ClaB1,MI1,[Lit|Path],[I|PI],PathLim,Lem,Set,Proof1) ), ( member(cut,Set) -> ! ; true ), prove(Cla,MI,Path,PI,PathLim,[Lit|Lem],Set,Proof2). % extension clause (e-clause) prove_ec((I^K)^V:ClaB,IV:Cla,MI,PI,ClaB1,MI1) :append(MIA,[(I^K1)^V1:Cla1|MIB],MI), length(PI,K), ( ClaB=[J^K:[ClaB2]|_], member(J^K1,PI), unify_with_occurs_check(V,V1), Cla=[_:[Cla2|_]|_], append(ClaD,[J^K1:MI2|ClaE],Cla1), prove_ec(ClaB2,Cla2,MI2,PI,ClaB1,MI3), append(ClaD,[J^K1:MI3|ClaE],Cla3), append(MIA,[(I^K1)^V1:Cla3|MIB],MI1) ; (\+member(I^K1,PI);V\==V1) -> ClaB1=(I^K)^V:ClaB, append(MIA,[IV:Cla|MIB],MI1) ). Regularity and Lemmata The regularity condition is implemented in line 20. In order to avoid backtracking, it is restricted to ground literals, i.e. literals without term variables or literals whose term variables have been substituted by terms that do not contain term variables. The lemma rule is implemented in line 22. Furthermore, the list Lem containing all literals that have been “solved” so far is added to the arguments of the prove predicate. In line 34 the current literal Lit is added as lemma to the set Lem. Restricted Backtracking The restricted backtracking technique for start clauses is implemented in line 2 and 3. Restricted backtracking for the reduction and extension rule (and the lemma rule) is implemented in line 33. In the former case an implicit Prolog cut in an if-then-else condition is used to cut off alternative start clauses, in the latter case a Prolog cut is used to cut off alternative connections. In both cases, restricted backtracking can be switched on or off (see below for details).
Positive and Conjecture Start Clauses By default, start clauses are restricted to positive clauses (lines 3 and 5). The predicate positiveC(Cla,Cla1) returns a positive start clause Cla1 if clause Cla is positive. It is implemented within another seven lines of Prolog code. If start clauses are restricted to conjecture clauses, a “!” is inserted into the matrix to split the clauses of the conjecture formula from the axiom clauses. In this case only clauses in front of the “!” are considered as start clauses (lines 2 and 4). See the full source code on the nanoCoP website for details.
Reordering Clauses By default, clauses are arranged in ascending order according to the number of paths through its elements. If reordering of clauses is switched on (see Section 4), all (sub-)clauses are reordered using a compact shuffle algorithm. It is implemented within 13 lines of Prolog code; see the full source code for details. Strategy Scheduling The argument Set of the prove predicate (see, e.g., lines 1, 7, 13, and 18) defines a strategy. It is a list of options and may contain the following elements: – “scut” (switch on restricted backtracking for start clauses), – “cut” (switch on restricted backtracking for reduction, extension and lemma rule), – “conj” (use conjecture start clauses), – “reo(J)” for J 2 IN (reorder the clauses J times before the proof search starts), and – “comp(I)” for I 2 IN (restart proof search using a complete search strategy, i.e. without scut, cut, and conj, if PathLim exceeds I).
These are the main strategies used for the fixed strategy scheduling together with the total time ratio allotted to them: [cut,comp(7)]/15%, [reo(22),conj,cut]/20%, [scut]/10%, [scut,cut]/5%, [reo(20),conj,cut]/10%, [reo(30),conj,scut,cut]/ 10%, and [reo(34),conj,scut,cut]/5%. Afterwards, 12 different strategies are invoked for 20% of the total time. Finally, the strategy [] is used for the remaining time ( 5%). As the first strategy and the last strategy are complete, the whole prover is complete (provided an arbitrary large total time is given). The strategy scheduling is implemented with a shell script that invokes the Prolog prover.
The different optimization techniques described in Section 3 and implemented in
Section 4 were evaluated on all 8044 first-order (so-called FOF) problems in the TPTP
library v6.4.0 [
Evaluation of Different Optimizations The following versions of nanoCoP are evaluated: a version without regularity and lemmata (“basic”), the standard version using regularity and lemmata (i.e. strategy [ ]), a version with conjecture start clauses ([conj]), two versions with restricted backtracking ([scut] and [cut]), nanoCoP 1.0, which uses only the strategy [cut,comp(7)], a version with reordering clauses (“reo”=[reo(22),conj,cut]), and nanoCoP 1.1 using the strategy scheduling described in Section 4.
Table 1 shows the results of the evaluation for a CPU time limit of 10 seconds. The table shows the number of proved (valid) problems (i.e. with TPTP status “Theorem” or “Unsatisfiable”) and the number of refuted (invalid) problems (i.e. with TPTP status “Countersatisfiable” or “Satisfiable”). The entry “errors” shows the number of problems for which nanoCoP terminates with a stack overflow error by Prolog. It also shows the number of new problems (“new proved”) that were not proved by a preceding version (“compared to”) of nanoCoP.
Whereas regularity and lemmata ([ ]) show only a small improvement,
conjecture start clauses ([conj]) and restricted backtracking ([scut] and [cut]) are very
effective techniques proving many more problems. For example, the [cut] version
proves 421 new problems compared to the standard version ([ ]). Using the strategy
[cut,comp(7)], nanoCoP 1.0 combines the [ ] and the [cut] techniques. The “reo”
version proves 242 new problems compared to nanoCoP 1.0, showing that reordering
clauses and conjecture start clauses are effective techniques as well. Using a strategy
scheduling, which is limited to the CPU time limit of 10 seconds (i.e., not all 20
strategies are used), nanoCoP 1.1 proves significantly more problems than nanoCoP 1.0.
The performance of nanoCoP 1.1 is compared to the following provers: the lean
(nonclausal) tableau prover leanTAP 2.3 [
Table 2 shows the results of the evaluation for a CPU time limit of 100 seconds (the
strategy scheduling of leanCoP 2.2 and nanoCoP 1.1 are adapted to this limit). The
entry “errors” shows the number of problems for which the prover terminated
without result before the CPU time limit was exceeded, e.g., because of a stack overflow
(leanTAP, leanCoP, and nanoCoP) or an empty set-of-support (Prover9). nanoCoP 1.1
proves slightly less problems than Prover9 and about the same number of problems as
leanCoP. The advantage of dealing directly with a non-clausal form is compensated
by the overhead for dealing with the non-clausal data structure. Only few problems in
the TPTP library are in a (deeply) nested non-clausal form; in this case proofs found
by nanoCoP can be significantly shorter than the clausal proofs found by leanCoP [
The paper presented a few effective optimization techniques for non-clausal connection calculi and described their integration into the nanoCoP prover. Together with a strategy scheduling, these techniques are the basis for the nanoCoP 1.1 prover. It solves almost 400 more problems from the TPTP library than the first version of nanoCoP, which essentially consists only of the Prolog core prover.
Future work include an improved representation of the clauses stored in Prolog’s
database and the integration of further techniques to prune the search space, such as
learning [
Acknowledgements. The author would like to thank Michael Fa¨rber for many useful discussions on the nanoCoP prover.