nanoCoP: Natural Non-clausal Theorem Proving

1 Introduction

Automated Theorem Proving (ATP) in classical first-order logic is a core research area in the field of Automated Reasoning (see [Robinson and Voronkov, 2001] for an overview). It is concerned with the question whether a conjecture H is a logical consequence of a given set of axioms G1, . . . ,Gn, written G1, . . . ,Gn |= H, in which G1, . . . ,Gn,H are firstorder formulae. More specifically the objective in ATP is to find a proof for the validity of a given formula F. A formula F is valid if and only if it evaluates to true for all possible interpretation of its function and predicate symbols. According to the Deduction Theorem (for classical logic), G1, . . . ,Gn |= H holds if and only if there is a proof for the validity of the formula (G1 ∧ . . . ∧ Gn) ⇒ H. A formal description of the proof search algorithm is usually specified in form of a proof (search) calculus consisting of axioms and rules. Implementations of such proof calculi are called ATP systems or (automated theorem) provers.

Most efficient fully automated theorem provers implement proof calculi that require the input formula to be in a clausal form, i.e. disjunctive or conjunctive normal form. Formulae that are not in clausal form are translated into clausal form in a preprocessing step. For example, the formula F#

has the disjunctive normal form (quantifiers are eliminated)

While the use of a clausal form technically simplifies the proof calculi and their implementations, it has some fundamental disadvantages. The standard translation into clausal form as well as the definitional translation [Plaisted and Greenbaum, 1986; Eder, 1992], which introduces definitions for subformulae, cause a significant overhead for the proof search [Otten, 2010]. For example, the disjunctive normal form of F#, in which some parts of the formula are copied, has more than twice the size of the original formula. Furthermore, a translation into clausal form modifies the structure of the formula, hence, a translation of the clausal proof back into one of the original formula is not straightforward [Reis, 2015]. On the other hand, proof search with more "natural" non-clausal calculi, such as sequent or standard tableau calculi [Gentzen, 1935; H¨ahnle, 2001] is less efficient.

This paper describes the non-clausal prover nanoCoP for classical first-order logic [Otten, 2016]. By performing the proof search on the original structure of the input formula, it combines the advantages of more natural non-clausal calculi with the efficiency of a goal-oriented connection-based proof search. The prover is based on a non-clausal connection calculus [Otten, 2011] (Section 2) that generalizes the clausal connection calculus [Bibel, 1983; 1987] and is implemented in a very compact way (Section 3). It follows the lean methodology already used for the clausal connection prover leanCoP, whose minimal Prolog source code is shown in Figure 1. An experimental evaluation (Section 4) indicates a solid performance of nanoCoP.

prove(I,S):- \+member(scut,S) -> 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<I -> true ; \+p -> assert(p), fail), prove(F,[L|P],I,Q,S) ), (member(cut,S) -> ! ; true), prove(C,P,I,[L|Q],S).

2 The Non-clausal Connection Calculus

The standard notation for first-order formulae is used. Terms (denoted by t) are built up from functions (f, g, h, i), constants (a, b, c), and variables (x, y, z). An atomic formula (A) is built up from predicate symbols (P,Q,R, S) and terms; a (first-order) formula (F, G, H) is built up from atomic formulae, the connectives ¬, ∧, ∨, ⇒, and the first-order quantifiers ∀ and ∃. 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 term substitution σ assigns terms to variables. A formula in clausal form has the form ∃x1 . . . ∃xn(C1∨. . .∨Cn), where each clause Ci is a conjunction of literals L1, . . . , Lmi . It is represented as a set of clauses {C1, . . . ,Cn}, called a (clausal) matrix. A polarity 0 or 1 is used to represent negation, i.e. literals of the form A and ¬A are represented by A0 and A1 , respectively, A connection is a set {A0 , A1 } of literals with the same predicate symbol but different polarities.

In a non-clausal matrix, a clause consists of literals and (sub)matrices. Let F be a formula and pol be a polarity. The non-clausal matrix M(F pol ) of a formula F pol is a set of clauses, in which a clause is a set of literals and matrices, and is defined according to Table 1. In Table 1, x∗ is a new variable, t∗ is the skolem term f ∗ (x1, . . . , xn) in which f ∗ is a new function symbol and x1, . . . , xn are the free variables in ∀xG or ∃xG. In G[x\t] all free occurrences of x in G are replaced by t. The non-clausal matrix M(F) of a formula F is the matrix M(F 0 ). In the graphical representation its clauses are arranged horizontally, while the literals and matrices of each clause are arranged vertically. For example, the formula F# of Section 1 has the simplified (i.e. redundant brackets are removed) non-clausal matrix M# =M(F#):

The graphical representation of the matrix M# is depicted in Figure 2. It already contains a clause copy with the fresh variable y′ and represents a non-clausal connection proof using the term substitution σ with σ(y) = a and σ(y′ ) = g(a); literals of each connection are connected with a line.

Compared to the formal clausal connection calculus [Otten and Bibel, 2003], a decomposition rule is added to the nonclausal calculus and the extension rule is slightly modified.

⎡⎢⎢⎢⎢⎣

⎤⎥⎥⎥⎥⎦

A clause C contains a literal L if and only if (iff) L∈C or C ′ contains L for M ′ ∈C, C ′∈M ′ . A clause C is α-related to a literal L iff it contains a matrix M ′ with {C ′ ,C ′′ }⊆M ′ for clauses C ′ ,C ′′ , such that C ′ contains L and C ′′ contains C (or C=C ′′ ). A copy of the clause C in the matrix M is made by renaming all free variables in C. M[C1\C2] denotes the matrix M, in which the clause C1 is replaced by C2. C ′ is a parent clause of C iff M ′ ∈C ′ and C ∈M ′ for some M ′ .

Let M be a matrix and Path be a set of literals. C is an extension clause (e-clause) of the matrix M with respect to a set of literals Path iff either (a) C contains a literal of Path, or (b) C is α-related to all literals of P ath occurring in M and if C has a parent clause, it contains a literal of Path. In the βclause of C2 with respect to L2, denoted by β-clauseL2 (C2), L2 and clauses that are α-related to L2 are deleted from C2.

The non-clausal connection calculus [Otten, 2011], which is sound and complete, is shown in Figure 3. Therein, M is a non-clausal matrix, C is a (subgoal) clause or ε (a special empty symbol) and (the active) Path is a set of literals or ε; σ is a term substitution. A non-clausal connection proof of M is a non-clausal connection proof of ε,M, ε.

The analytic, i.e. bottom-up, proof search is carried out in the same way as in the clausal calculus. Additional backtracking might be required when selecting C1 in the decomposition rule, but no backtracking is required when selecting M1. The rigid, i.e. single, term substitution σ is calculated whenever a connection is identified in a reduction or extension rule. On formulae in clausal form, the non-clausal connection calculus coincides with the clausal connection calculus.

3 The nanoCoP TheoremProver

The implementation of the non-clausal connection calculus of Figure 3 follows the lean methodology [Beckert and Posegga, 1995], which is already used for the clausal connection prover leanCoP [Otten and Bibel, 2003]. It uses very compact Prolog code to implement the basic calculus and adds a few essential optimization techniques in order to prune the search space. The resulting natural nonclausal connection prover nanoCoP is available under the GNU General Public License and can be downloaded at http://www.leancop.de/nanocop/ .

In a first step, the input formula F is translated into a nonclausal (indexed) matrix M(F) according to Table 1; redundant brackets are removed [Otten, 2011]. Additionally, every (sub-)clause (I, V ) : C and (sub-)matrix J :M is marked with a unique index I or J; clause C is also marked with a set of variables V that are newly introduced in C but not in any subclause of C. Atomic formulae are represented by Prolog atoms, term variables by Prolog variables and the polarity 1 by "-". Sets, e.g. clauses and matrices, are represented by Prolog lists (representing multisets). For example, the matrix M# from Section 2 is represented by the Prolog term

[(0ˆK)ˆ[]:[-(p(a))], (1ˆK)ˆ[]:[2ˆK:[(3ˆK)ˆ[Y]:[p(Y),-(p(g(Y)))]], 4ˆK:[(5ˆK)ˆ[]:[q],(6ˆK)ˆ[]:[-q]], 7ˆK:[(8ˆK)ˆ[]:[r],(9ˆK)ˆ[]:[-r]]], (10ˆK)ˆ[]:[p(g(g(a)))]]

in which the Prolog variable K is used to enumerate clause copies. In the second step, the matrix M =M(F) is written into Prolog's database. For every literal Lit in M the fact

lit(Lit,ClaB,ClaC,Grnd)

is asserted into the database where ClaC ∈ M is the (largest) clause in which Lit occurs and ClaB is the β-clause of ClaC with respect to Lit. Grnd is set to g if the smallest clause in which Lit occurs is ground, i.e. does not contain any variables; otherwise Grnd is set to n. Storing literals of M in the database in this way is called lean Prolog technology [Otten, 2010] and integrates the advantages of the Prolog technology approach [Stickel, 1988] into the lean theorem proving framework. No other modifications or simplifications of the original formula are done during these two preprocessing steps.

The nanoCoP source code is shown in Figure 4. As an optimization, it uses positive start clauses [Otten, 2011], calculated by the predicate positiveC(Cla,Cla1).

The predicate prove(Mat,PathLim,Set,Proof) implements the start rule. Mat is the matrix generated in the preprocessing step, PathLim is the maximum size of the active path used for iterative deepening, and Proof contains the returned connection proof. Set is a list of options used to control the restricted backtracking technique [Otten, 2010] and may contain "cut" and "comp(I)" for I ∈IN. In order to achieve completeness, nanoCoP performs an iterative deepening on the size of the active path implemented within the second Prolog clause of this prove predicate.

The predicate prove(Cla,Mat,Path,PathI,PathLim, Lem,Set,Proof) implements the axiom, the decomposition rule, the reduction rule, and the extension rule of the non-clausal connection calculus of Figure 3. Cla, Mat, and Path represent the subgoal clause C, the (indexed) matrix M and the (active) Path. The term substitution σ is stored implicitly by Prolog. The indexed path PathI contains the indices of all clauses and matrices that contain literals of Path; it is used for calculating extension clauses. The list Lem is used for the lemmata rule and contains all literals that have already been "solved" [Otten, 2010]. This prove predicate succeeds iff there is a connection proof for the tuple Cla, Mat, Path with |Path|< PathLim. In this case Proof returns a connection proof. The input matrix Mat has to be stored in Prolog's database as explained above.

Finally, the last predicate prove_ec(ClaB,Cla1,Mat, PathI,ClaB1,Mat1) is used to calculate extension clauses. Starting with the (largest possible) extension clause Cla1, its β-clause ClaB, the current (indexed) matrix Mat, and the indexed path PathI, it returns an appropriate extension clause Cla, copies it into Mat and returns its β-clause ClaB1 and the new (indexed) matrix Mat1.

nanoCoP uses additional optimization techniques that are already used in the clausal connection prover leanCoP: regularity, lemmata, and restricted backtracking [Otten, 2010].

% start rule prove(Mat,PathLim,Set,[(Iˆ0)ˆV:Cla1|Proof]) :- 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) ).

4 Experimental Evaluation

The following evaluations were conducted on a 3.4 GHz Xeon system with 4 GB of RAM running Linux 3.13.0 and ECLiPSe Prolog 5.10. The CPU time limit for all proof attempts was set 100 seconds.

The following formula Fn is a slightly extended version of the formula F# of Section 1, where f n , gn , hn , and in are abbreviations for n nested applications of these functions:

Table 2 shows the timings on this (valid) formula class for n=10, n=30, and n=90 for the following provers: the lean (non-clausal) tableau prover leanTAP [Beckert and Posegga, 1995], the resolution prover Prover9 [McCune, 2005], the superposition prover E [Schulz, 2002] (using options "--auto --tptp3-format"), the clausal connection prover leanCoP [Otten and Bibel, 2003; Otten, 2010], and nanoCoP. The leanCoP core prover with the standard ("[nodef]") and the definitional ("[def]") translation into clausal form were tested. For nanoCoP restricted backtracking was switched off (Set=[]). Times are given in seconds; the size of the returned proof tree, i.e. the number of nodes of the proof tree, is given in brackets.

The last line of Table 2 shows the number of proved problems of all 5051 first-order (FOF) problems in the TPTP library v3.7.0 [Sutcliffe, 2009]. For leanTAP, leanCoP, and nanoCoP, the required equality axioms were added in a preprocessing step (which is included in the timings). The nanoCoP core prover performs significantly better than both clausal form translations of the leanCoP core prover.

Furthermore, 40%/51% of the proofs found by nanoCoP are shorter than those of leanCoP [nodef]/[def], respectively; as many of the problems in the TPTP library are "mostly" in a clausal form, 56%/47% of the proofs have the same size. The proofs of nanoCoP are up to 96%/74% shorter than those of the leanCoP versions [nodef]/[def], respectively.

The "full" leanCoP 2.2 prover, which additionally uses a strategy scheduling [Otten, 2010], proves 1710 TPTP problems. The version of nanoCoP using a restricted backtracking strategy, i.e. Set=[cut,comp(6)], was tested as well; it proves 1485 TPTP problems.

Tests have also shown that the classical version of the non-clausal connection prover JProver [Schmitt et al., 2001], which is the only published non-clausal connection prover so far, has a lower performance than leanTAP.

5 Conclusion

Formal reasoning is a fundamental task in mathematics, computer science and many related fields. Since Frege published the first formal calculus for first-order logic in his Begriffsschrift [Frege, 1879], the development and implementation of efficient proof calculi has made significant progress. But up to now, most -if not all- efficient fully automated theorem provers for classical first-order logic translate the input formula into a clausal form. By using the standard translation the size of the resulting formula can grow exponentially with respect to the size of the original formula. Even a definitional translation increases the size of the formula, which results in a significant overhead for the proof search [Otten, 2010]. Both clausal form translations modify the structure of the formula, making it difficult to translate the (clausal) proof back into a proof of the original formula.

This paper introduced nanoCoP, the first efficient nonclausal connection prover for classical first-order logic. Using non-clausal matrices the proof search works directly on the original structure of the input formula and, thus, avoids a translation into any clausal form. This combines the advantages of more natural non-clausal sequent or tableau provers with the goal-oriented efficiency of connection provers.

Even though the non-clausal inferences introduce a slight overhead, nanoCoP outperforms both clausal form translations of the leanCoP core prover on a large set of TPTP problems. About half of the returned non-clausal proofs are up to 96% shorter than their clausal counterparts.

nanoCoP returns a compact non-clausal connection proof. A connection corresponds to a closed branch in the tableau calculus [H¨ahnle, 2001] or an axiom in the sequent calculus [Gentzen, 1935]. Hence, the translation into, e.g., a sequent proof is straightforward. The compact size of nanoCoP makes it also a suitable tool for the development of verifiably correct software [Otten and Bibel, 2017], as its correctness can be proven much more easily than that of an ATP system consisting of several thousand lines of source code.

Only few research work investigates non-clausal connection calculi and implementations. Other approaches [Andrews, 1981; Bibel, 1987; H¨ahnle et al., 2004; Kreitz and Otten, 1999] work (efficiently) only for ground formulae or their implementation is not available anymore [Issar, 1990].

Another important application of nanoCoP is its usage within non-classical logics, such as (first-order) intuitionistic or modal logic, for which the use of a clausal form is either not desirable or not possible. Hence, future work includes the combination of the non-clausal approach with the prefix (unification) technique for some non-classical logics, as already done for leanCoP [Otten, 2008; 2014]. In order to improve performance, further optimization techniques need to be integrated into nanoCoP, such as strategy scheduling [Otten, 2010], learning [Kaliszyk and Urban, 2015] or variable splitting [Antonsen and Waaler, 2007].

Acknowledgements

The author would like to thank Wolfgang Bibel for his helpful comments on a preliminary version of this paper.