System Description: The Cut-Elimination System CERES ∗

Abstract

Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton of an LK-proof with only atomic cuts. The use of resolution and the enormous size of (formalized) mathematically relevant proofs suggest an implementation able to handle rather complex cut-elimination problems. In this paper we present an implementation of CERES: the system CERES. It already implements an improvement based on an extension of LK to the calculus LKDe containing equality rules and rules for introduction of definitions which makes it easier to formalize and interpret mathematical proofs in LK. Furthermore it increases the efficiency of the cut-elimination method. The system CERES already performs well in handling quite large proofs.

Introduction

Proof analysis is a central mathematical activity which proves crucial to the development of mathematics. Indeed many mathematical concepts such as the notion of group or the notion of probability were introduced by analyzing existing arguments. In some sense the analysis and synthesis of proofs form the very core of mathematical progress [ 12, 13 ].

Cut-elimination introduced by Gentzen [8] is the most prominent form of proof transformation in logic and plays an important role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas) from proofs resulting in a proof which is analytic in the sense, that all statements in the proof are subformulas of the result. Therefore, the proof of a combinatorial statement is converted into a purely combinatorial proof. Cut elimination is therefore an essential tool for the analysis of mathematical proofs, especially to make implicit parameters explicit. Cut free derivations allow for • the extraction of Herbrand disjunctions, which can be used to establish bounds on existential quantifiers (e.g. Luckhardt’s analysis of the Theorem of Roth [ 11 ]). • the construction of interpolants, which allow for the replacement of implicit definitions by explicit definitions according to Beth’s Theorem. • the calculation of generalized variants of the end formula.

In a formal sense Girard’s analysis of van der Waerden’s theorem [ 9 ] is the application of cut-elimination to the proof of Fu¨rstenberg/Weiss with the “perspective” of obtaining van der Waerden’s proof. Indeed an application of a complex proof transformation like cut-elimination by humans requires a goal oriented strategy.

Note that cut-elimination is non-unique, i.e. there is no single cut-free proof which represents the analytic version of a proof with lemmas. Therefore the application of purely computational methods on existing proofs may even produce new interesting proofs. Indeed, it is non-uniqueness which makes computational experiments with cutelimination interesting [ 3 ]. The experiments can be considered as a source for a base of proofs in formal format which provide different mathematical and computational information.

CERES [ 5, 6 ] is a cut-elimination method that is based on resolution. The method roughly works as follows: The structure of the proof containing cuts is mapped to an unsatisfiable set of clauses C (the characteristic clause set). A resolution refutation of C, which is obtained using a first-order theorem prover, serves as a skeleton for the new proof which contains only atomic cuts. In a final step also these atomic cuts can be eliminated, provided the (atomic) axioms are valid sequents; but this step is of minor mathematical interest and of low complexity. In the system CERES1 this method of cutelimination has been implemented. The system is capable of dealing with formal proofs in an extended version of LK, among them also very large ones (i.e. proofs with more than 1500 nodes and cut-elimination has been done within 14 seconds).

The extension of CERES to LKDe a calculus containing definition introductions and equality rules [ 10 ] moves the system closer to real mathematical proofs. In particular, introduction of definitions and concepts is perhaps the most significant activity of a mathematician in structuring proofs and theories. By its high efficiency (the core of the method is first-order theorem proving by resolution and paramodulation) CERES might become a strong tool in automated proof mining and contribute to an experimental culture of computer-aided proof analysis in mathematics.

1available at http://www.logic.at/ceres/

The System CERES

The cut-elimination system CERES is written in ANSI-C++. There are two main tasks. One is to compute an unsatisfiable set of clauses characterizing the cut formulas. This is done by automatically extracting the so-called characteristic clause set CL(ϕ). The other is to generate a resolution refutation of CL(ϕ) by an external theorem prover2, and to compute the necessary projections of ϕ w.r.t. the clauses in CL(ϕ) actually used for the refutation. A projection of ϕ modulo a clause C ∈ CL(ϕ) is gained by applying all inference rules of ϕ not operating on cut ancestors to the initial sequents of C. The properly instantiated projections are concatenated, using the refutation obtained by the theorem prover as a skeleton of a proof with only atomic cuts.

The extraction of the characteristic clause set CL(ϕ) from an LKDe-proof ϕ is defined inductively. For every node ν of ϕ either: • If ν is an occurrence of an axiom S and S′ is the subsequent of S containing only ancestors of cut formulas then Cν = { S′ }. • Let ν1, ν2 be the predecessors of ν in a binary inference then we distinguish: – The auxiliary formulas of ν1, ν2 are ancestors of cut formulas then Cν =

Cν1 ∪ Cν2 . – Otherwise Cν = Cν1 × Cν2 , where C × D = { C ◦ D | C ∈ C, D ∈ D } and C ◦ D is the merge of the clauses C and D.

• Let ν′ be the predecessor of ν in a unary inference then Cν = Cν′ .

The characteristic clause set CL(ϕ) is defined as Cν where ν is the root node of ϕ.

The definition rules of LKDe directly correspond to the extension principle (see [7]) in predicate logic. It simply consists in introducing new predicate- and function symbols as abbreviations for formulas and terms. Mathematically this corresponds to the introduction of new concepts in theories. Let A be a first-order formula with the free variables x1, . . . , xk (denoted by A(x1, . . . , xk) and P be a new k-ary predicate symbol (corresponding to the formula A). Then the rules are:

A(t1, . . . , tk), Γ ⊢ Δ P (t1, . . . , tk), Γ ⊢ Δ defP : l Γ ⊢ Δ, A(t1, . . . , tk) Γ ⊢ Δ, P (t1, . . . , tk) defP : r for arbitrary sequences of terms t1, . . . , tk. There are also definition introduction rules for new function symbols which are of similar type. The equality rules are: Γ1 ⊢ Δ1, s = t A[s]Λ, Γ2 ⊢ Δ2

A[t]Λ, Γ1, Γ2 ⊢ Δ1, Δ2 Γ1 ⊢ Δ1, t = s A[s]Λ, Γ2 ⊢ Δ2

A[t]Λ, Γ1, Γ2 ⊢ Δ1, Δ2 for inference on the left and Γ1 ⊢ Δ1, s = t Γ2 ⊢ Δ2, A[s]Λ Γ1, Γ2 ⊢ Δ1, Δ2, A[t]Λ Γ1 ⊢ Δ1, t = s Γ2 ⊢ Δ2, A[s]Λ

Γ1, Γ2 ⊢ Δ1, Δ2, A[t]Λ =: l1 =: r1 =: l2 =: r2 2The current version of CERES uses the automated theorem prover Otter (see http://www-unix.mcs. anl.gov/AR/otter/), but any refutational theorem prover based on resolution and paramodulation may be used. on the right, where Λ denotes a set of positions of subterms where replacement of s by t has to be performed. We call s = t the active equation of the rules. Note that, on atomic sequents, the rules coincide with paramodulation – under previous application of the most general unifier.

Concerning the extension of the CERES-method from LK to LKDe, equality rules appearing within the input proof are propagated to the projections like any other binary rules. During theorem proving equality is treated by paramodulation; its application within the final clausal refutation is then transformed to the appropriate equality rules in LKDe. The definition introductions do not require any other special treatment within CERES than all other unary rules; in particular, they have no influence on the theorem proving part.

Since the restriction to skolemized proofs is crucial to the CERES-method, the system also performs skolemization (according to Andrew’s method [ 2 ]) on the input proof.

The system CERES expects an LKDe proof of a sequent S and a set of axioms as input, and, after validation of the input proof, computes a proof of S containing at most atomic-cuts. Input and output are formatted using the well known data representation language XML. This allows the use of arbitrary and well known utilities for editing, transformation and presentation and standardized programming libraries. To increase the performance and avoid redundancy, most parts of the proofs are internally represented as directed acyclic graphs. This representation turns out to be very handy, also for the internal unification algorithms.

The formal analysis of mathematical proofs (especially by a mathematician as a preand post-“processor”) relies on a suitable format for the input and output of proofs, and on an appropriate aid in dealing with them. We developed an intermediary proof language connecting the language of mathematical proofs with LKDe and the compiler HLK3 transforming proofs written in this higher-level language to LKDe. Furthermore we implemented a proof tool4 with a graphical user interface, allowing a convenient input and analysis of the output of CERES. Thereby the integration of definition- and equalityrules into the underlying calculus plays an essential role in overlooking, understanding and analyzing complex mathematical proofs by humans. 3

Example

The example proof below is taken from [ 14 ]; it was formalized in LK and analyzed by a former version of CERES in the paper [ 3 ]. Here we use the extensions by equality rules and definition-introduction in LKDe to give a simpler formalization and analysis of the proof. The end-sequent formalizes the statement: on a tape with infinitely many cells which are all labelled by 0 or by 1 there are at least two cells labelled by the same number. f (x) = 0 expresses that the cell number x is labelled by 0. Indexing of cells is done by number terms defined over 0, 1 and +. The proof ϕ below uses two lemmas: (1) there are infinitely many cells labelled by 0 and (2) there are infinitely many cells labelled by 1. The proof shows the statement by a case distinction: If there are infinitely many cells labelled by 0 then choose two of them, otherwise there are infinitely many

3available at http://www.logic.at/hlk/ 4available at http://www.logic.at/prooftool/

cells labelled by 1 and we can then choose two of them. In each case there are two cells with the same value. These lemmas are eliminated by CERES and a more direct argument is obtained in the resulting proof ϕ′. Ancestors of the cuts in ϕ are indicated in boldface.

Let ϕ be the proof (τ)

(ǫ0) A ⊢ I0,I1 I0 ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) cut I1 ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) cut (ǫ1) A ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)),I1

A ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) where τ = For τ′ =

(τ′) A ⊢ f(n0 + n1) = 0,f(n1 + n0) = 1 A ⊢ f(n0 + n1) = 0,∃k.f(n1 + k) = 1 ∃r A ⊢ ∃k.f(n0 + k) = 0,∃k.f(n1 + k) = 1 ∃r A ⊢ ∃k.f(n0 + k) = 0,∀n∃k.f(n + k) = 1 ∀:r A ⊢ ∀n∃k.f(n + k) = 0,∀n∃k.f(n + k) = 1 ∀:r

A ⊢ I0,∀n∃k.f(n + k) = 1 defI0:r

A ⊢ I0,I1 defI1:r

(Axiom) ⊢ n1 + n0 = n0 + n1 f(n1 + n0) = 1 ⊢ f(n1 + n0) = 1 f(n0 + n1) = 0 ⊢ f(n0 + n1) = 0 f(n0 + n1) = 1 ⊢ f(n1 + n0) = 1 f(n0 + n1) = 0 ∨ f(n0 + n1) = 1 ⊢ f(n0 + n1) = 0,f(n1 + n0) = 1 ∨:l ∀x(f(x) = 0 ∨ f(x) = 1) ⊢ f(n0 + n1) = 0,f(n1 + n0) = 1 ∀:l

A ⊢ f(n0 + n1) = 0,f(n1 + n0) = 1 defA:l =:l1 And for i = 1,2 we define the proofs ǫi =

ψ ηi f(s) = i,f(t) = i ⊢ s 6= t ∧ f(s) = f(t) ∧:r f(s) = i,f(t) = i ⊢ ∃q(s 6= q ∧ f(s) = f(q)) ∃:r f(s) = i,f(t) = i ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) ∃:r f(n0 + k0) = i,∃k.f(((n0 + k0) + 1) + k) = i ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) ∃:l f(n0 + k0) = i,∀n∃k.f(n + k) = i ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) ∀:l ∃k.f(n0 + k) = i,∀n∃k.f(n + k) = i ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) ∃:l ∀n∃k.f(n + k) = i,∀n∃k.f(n + k) = i ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) ∀:l c:l ∀n∃k.f(n + k) = i ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) defIi:l

Ii ⊢ ∃p∃q(p 6= q ∧ f(p) = f(q)) for s = n0 + k0, t = ((n0 + k0) + 1) + k1, and the proofs ψ =

(axiom) (axiom) ⊢ (n0 + k0) + (1 + k1) = ((n0 + k0) + 1) + k1 n0 + k0 = (n0 + k0) + (1 + k1) ⊢ n⊢0n+0 +k0k=06=((n((0n+0 +k0k)0+) +1)1+) +k1k⊢1 ¬:r =:l1 and ηi = The characteristic clause set is (after variable renaming)

CL(ϕ) = {⊢ f (x + y) = 0, f (y + x) = 1; (C1) f (x + y) = 0, f (((x + y) + 1) + z) = 0 ⊢; (C2) f (x + y) = 1, f (((x + y) + 1) + z) = 1 ⊢} (C3).

The axioms used for the proof are the standard axioms of type A ⊢ A and instances of ⊢ x = x, of commutativity ⊢ x + y = y + x, of associativity ⊢ (x + y) + z = x + (y + z), and of the axiom

x = x + (1 + y) ⊢, expressing that x + (1 + y) 6= x for all natural numbers x, y.

The comparison with the analysis of Urban’s proof formulated in LK (without equality) [ 3 ] shows that the proof based on equality is much more transparent. In fact the set of characteristic clauses contains only 3 elements (instead of 5), which are also simpler. This also facilitates the refutation of the clause set and makes the output proof simpler and more transparent. On the other hand, the analysis below shows that the mathematical argument obtained by cut-elimination is the same as in [ 3 ].

The program Otter found the following refutation of CL(ϕ) (based on hyperresolution only — without equality inference):

The first hyperesolvent, based on the clash sequence (C2; C1, C1), is C4 = D1 = ⊢ f (y + x) = 1, f (z + ((x + y) + 1)) = 1, with the intermediary clause f (((x + y) + 1) + z) = 0 ⊢ f (y + x) = 1.

The next clash is sequence is (C3; C4, C4) which gives C5 with intermediary clause D2, where:

C5 = D2 = ⊢ f (v′ + u′) = 1, f (v + u) = 1, f (x + y) = 1 ⊢ f (v + u) = 1.

Factoring C5 gives C6: ⊢ f (v +u) = 1 (which roughly expresses that all fields are labelled by 1). The final clash sequence (C3; C6, C6) obviously results in the empty clause ⊢ with intermediary clause D3: f (((x + y) + 1) + z) = 1 ⊢. The hyperresolution proof ψ3 in form of a tree can be obtained from the following resolution trees, where C′ and ψ′ stand for renamed variants of C and of ψ, respectively:

C1

D1

C2 res

C4

′ C1 res ψ2: = ψ3: =

ψ1 D2 res Instantiation of ψ3 by the uniform most general unifier σ of all resolutions gives a deduction tree ψ3σ in LKDe; indeed, after application of σ, resolution becomes cut and factoring becomes contraction. The proof ψ3σ is the skeleton of an LKDe-proof of the end-sequent with only atomic cuts. Then the leaves of the tree ψ3σ have to be replaced by the proof projections. E.g., the clause C1 is replaced by the proof ϕ[C1], where s = n0 + n1 and t = n1 + n0: Note that ψ, η0, η1 are the same as in the definition of ǫ0, ǫ1 above.

By inserting the σ-instances of the projections into the resolution proof ψ3σ and performing some additional contractions, we eventually obtain the desired proof ϕ′ of the end-sequent

A ⊢ ∃p∃q(p 6= q ∧ f (p) = f (q)) with only atomic cuts. ϕ′ no longer uses the lemmas that infinitely many cells are labelled by 0 and by 1, respectively. 4

Intended Extensions of CERES And Future Work

We plan to develop the following extensions of CERES: • As the cut-free proofs are often very large and difficult to interpret, we intend to provide the possibility to analyze certain characteristics of the cut-free proof (which are simpler than the proof itself). An important example are Herbrand sequents which may serve to extract bounds from proofs (see e.g. [ 11 ]). We plan to develop algorithms for extracting Herbrand sequents (also from proofs of nonprenex sequents as indicated in [ 4 ]) and for computing interpolants, which allow for the replacement of implicit definitions by explicit ones according to Beth’s Theorem. • In the present version CERES eliminates all cuts at once. But - for the application to real mathematical proofs human user interaction is required — in particular only interesting cuts (i.e. lemmas of mathematical importance) deserve to be eliminated, others should be integrated as additional axioms. • As CERES requires the skolemization of the end-sequent the original proof must be transformed to Skolem form. We plan to develop an efficient reversed-skolemizationalgorithm, which transforms the theorem to be proved into its original form. • A great challenge in the formal analysis of mathematical proofs lies in providing a suitable format for the input and output of proofs. We plan to improve our intermediary proof language and to move closer to the “natural” language of mathematical proofs.

To demonstrate the abilities of CERES and the feasibility of formalizing and analyzing complex proofs of mathematical relevance, we currently investigate a well known proof of the infinity of primes using topology (which may be found in [ 1 ]). Our aim is to eliminate the topological concepts from the proof by means of CERES, breaking it down to a proof solely based on elementary number arithmetic. This way one can obtain new insights into the construction of prime numbers contained in the topological proof.

Mathematische

References

[1] M. Aigner , G. M. Ziegler: Proofs from THE BOOK . Springer, 1998 .

[2] P. B. Andrews : Resolution in Type Theory , Journal of Symbolic Logic , 36 , pp. 414 - 432 , 1971 .

[3] M. Baaz , S. Hetzl , A. Leitsch , C. Richter , H. Spohr: Cut-Elimination: Experiments with CERES , Proc. LPAR 2004 , pp. 481 - 495 , Springer, 2004 .

[4] M. Baaz , A . Leitsch: On Skolemization and Proof Complexity , Fundamenta Informaticae, 20 ( 4 ), pp. 353 - 379 , 1994 .

[5] M. Baaz , A. Leitsch: Cut-Elimination and Redundancy-Elimination by Resolution , Journal of Symbolic Computation , 29 , pp. 149 - 176 , 2000 .

[6] M. Baaz , A. Leitsch: Towards a Clausal Analysis of Cut-Elimination , Journal of Symbolic Computation , 41 , pp. 381 - 410 , 2006 .

[9] J. Y. Girard : Proof Theory and Logical Complexity, in Studies in Proof Theory , Bibliopolis, Napoli, 1987 .

[10] A. Leitsch , C. Richter: Equational Theories in CERES, unpublished (available at http://www.logic.at/ceres/), 2005 .

[11] H. Luckhardt : Herbrand-Analysen zweier Beweise des Satzes von Roth: polynomiale Anzahlschranken , The Journal of Symbolic Logic , 54 , pp. 234 - 263 , 1989 .

[12] G. Polya : Mathematics and plausible reasoning, Volume I: Induction and Analogy in Mathematics, Princeton University Press, Princeton, New Jersey, 1954 .

[13] G. Polya : Mathematics and plausible reasoning , Volume II: Patterns of Plausible Inference , Princeton University Press, Princeton, New Jersey, 1954 .

[14] C. Urban: Classical Logic and Computation Ph . D. Thesis , University of Cambridge Computer Laboratory, 2000 .