Introduction

Cut-elimination introduced by Gentzen [6] 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.

In a formal sense Girard's famous analysis of van der Waerden's theorem [7] consists in the application of cut-elimination to the proof of Fürstenberg and Weiss (which uses topological arguments) with the "perspective" of obtaining van der Waerden's elementary proof. Indeed, an application of a complex proof transformation like cut-elimination by humans requires a goal oriented strategy.

CERES [4,5] is a cut-elimination method that is based on resolution. The method roughly works as follows: The structure of an LK-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 (AC normal form). 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 cut-elimination has been implemented. The extension of CERES from LK to LKDe, a calculus containing definition introductions and equality rules (see [10] and [1]), moved the system closer to real mathematical proofs. The system CERES has been applied successfully to a well known mathematical proof, namely to Fürstenberg's proof of the infinity of primes [2]; it was shown that the elimination of topological arguments from the proof resulted in Euclid's famous proof. Though CERES did not (yet) produce substantial mathematical proofs previously unknown, the analysis of Fürstenberg's proof demonstrates the potential of the method to handle nontrivial mathematics.

The main task of the CERES-method is proof transformation, not just proof verification. For the latter one there are powerful higher-order systems like Isabelle2 (see [12]) and Coq 3 (see [11]); these Rudnicki P, Sutcliffe G., Konev B., Schmidt R., Schulz S. (eds.); Proceedings of the Combined KEAPPA -IWIL Workshops, pp. 77-91

Proofs in the CERES-system Hetzl, Leitsch, Weller, Woltzenlogel Paleo systems have been used successfully to verify complicated and famous mathematical proofs like this of the four color theorem (see http://research.microsoft.com/ ~gonthier/). The core algorithm of CERES, however, works on LK-proofs and performs cut-elimination. For this reason we have developed the higher proof language HLK which is close to the sequent calculus LK, making translations to LK easy and efficient.

In this paper we present the input-output environment of CERES and illustrate the interaction of users with the system. In the first step proofs are formalized in HLK. The formalized proof is then compiled to LKDe and analyzed by the CERES-algorithm, and finally the resulting atomic cut normal form can be viewed by Prooftool. Moreover, from the normal form a Herbrand sequent can be extracted which contains mathematical information in a more condensed form. We illustrate all phases of proof specification and analysis by an example, the tape proof of Christian Urban (see also [1]). steps are executed within the system and in interaction with the user:

System overview

1. The user (intended to be a mathematician with a background in logic) selects an interesting informal mathematical proof to be transformed and analyzed. Informal mathematical proofs are proofs in natural language, as they usually occur in mathematics.

2. The user writes the selected proof in HandyLK , a higher proof language, intermediary between natural mathematical language and formal calculi.

3. The HandyLK proof is input to the compiler HLK.

4.

HLK generates a formal proof in sequent calculus LKDe.

5.

The formal proof is input to CERES, which is responsible for all sorts of proof transformations, including cut-elimination.

6. CERES extracts from the formal proof a characteristic clause set, which contains clauses formed from ancestors of cut-formulas in the formal proof.

7. The characteristic clause set is then input to a resolution theorem prover, e.g. Otter4 or Prover95 .

8. The resolution theorem prover outputs a refutation of the characteristic clause set.

9. CERES receives the refutation, which will be used as a skeleton for the transformed proof in atomiccut normal form (ACNF).

10. CERES outputs the grounded refutation in a tree format and the characteristic clause set. Moreover it extracts projections from the formal proof and plugs them into the refutation in order to generate the ACNF. The projections and the ACNF are also output. A Herbrand sequent is obtained from the instantiation information of the quantifiers of the end-sequent (resulting in an (equationally) valid sequent) and output as well. The Herbrand sequent typically summarizes the creative content of the ACNF. For details, see [8].

11. All outputs and inputs of CERES can be opened with ProofTool.

12. ProofTool, a graphical user interface, renders all proofs, refutations, projections, sequents and clause sets so that they can be visualized by the user.

13. The information displayed via ProofTool is analyzed by the user.

14. Based on his analysis, the user can formulate new mathematical ideas, e.g. a new informal direct proof corresponding to the ACNF.

Proof analysis with CERES

Our calculus LKDe is based on standard LK with permutation, contraction and weakening, atomic axioms and multiplicative rules. For example, the following rules deal with the ∧-connective:

Γ ∆, A Π Λ, B Γ, Π ∆, Λ, A ∧ B ∧ : r A, Γ ∆ A ∧ B, Γ ∆ ∧ : l1 A, Γ ∆ B ∧ A, Γ ∆ ∧ : l2

In addition, to bring the calculus closer to mathematical practice, definition introduction and equality handling rules are used: Let A be a first-order formula with the free variables x 1 , . . . , x k (denoted by A(x 1 , . . . , x k )) and P be a new k-ary predicate symbol (corresponding to the formula A). Then the definition introduction rules are: The equality rules (also called paramodulation rules) are:

A(t 1 , . . . ,t k ), Γ ∆ P(t 1 , . . . ,t k ), Γ ∆ def P : l Γ ∆, A(Γ 1 ∆ 1 , s = t A[s] Λ , Γ 2 ∆ 2 A[t] Λ , Γ 1 , Γ 2 ∆ 1 , ∆ 2 = : l1 Γ 1 ∆ 1 ,t = s A[s] Λ , Γ 2 ∆ 2 A[t] Λ , Γ 1 , Γ 2 ∆ 1 , ∆ 2 = : l2

for inference on the left and

Γ 1 ∆ 1 , s = t Γ 2 ∆ 2 , A[s] Λ Γ 1 , Γ 2 ∆ 1 , ∆ 2 , A[t] Λ = : r1 Γ 1 ∆ 1 ,t = s Γ 2 ∆ 2 , A[s] Λ Γ 1 , Γ 2 ∆ 1 , ∆ 2 , A[t] Λ = : r2

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.

We will now introduce the CERES system by presenting the analysis of a proof from [13]; it was formalized in LKDe and analyzed by CERES in [1]. The end-sequent formalizes the statement: on a tape with infinitely many cells which are all labelled by 0 or by 1 there are two cells labelled by the same number. f (x) = 0 expresses that the cell nr. 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. These lemmas are eliminated by CERES and a more direct argument is obtained in the resulting proof ϕ .

Specifying proofs in HandyLK

In this section, we introduce the higher proof language HandyLK by presenting its most important features and syntax by means of our example proof. HandyLK is based on the idea that many aspects of writing LKDe proofs can be automatized. It supports a many-sorted first-order language.

Before starting to write proofs, it is first necessary to define the language and the function and predicate definitions one intends to use. In our example, we deal with a language with one sort (natural numbers) and the constants mentioned above. In HandyLK , we write: define type nat; define constant 0, 1 of type nat; define infix function + of type nat,nat to nat with weight 100; define function f of type nat to nat;

In the definition of infix functions like +, we may set a weight that allows terms to be written in the usual mathematical way, where superfluous brackets may be dropped. In addition to the constants, we define some variables that will be used in the proof. Here, the function f is the labelling function assigning labels to tape cells. define variable k, l, n, p, q, x, n_0, n_1 of type nat;

We also define the axioms we will use. Note that :-represents in HandyLK .

define axiom :-k + l = l + k; define axiom :-k + (l + n) = (k + l) + n; define axiom k = k + (1 + l) :-; define axiom :-k = k;

Finally, we introduce some predicate definitions.

define predicate A by all x ( f(x) = 0 or f(x) = 1 ); define predicate I by all n ex k f( n + k ) = x; Note that in the definition of I, x is a free variable. The free variables determine the arity of the defined predicate, and can be instantiated by parameters. If P is a defined predicate, F is its defining formula and x are the free variables of F, then the predicate definition is interpreted as ∀ x(P( x) ⇐⇒ F). In our example, the predicate A is the assumption: All cells are labelled either 0 or 1. The predicate I(x) states that there are infinitely many cells labelled x.

We now turn to formalizing our example proof ϕ. In LKDe, ϕ is

(τ) A I(0), I(1) (ε(0)) I(0) ∃p∃q(p = q ∧ f (p) = f (q)) A ∃p∃q(p = q ∧ f (p) = f (q)), I(1) cut (ε(1)) I(1) ∃p∃q(p = q ∧ f (p) = f (q)) A ∃p∃q(p = q ∧ f (p) = f (q)) cut

Here τ is a proof of the fact that either infinitely many cells are labelled 0, or infinitely many cells are labelled 1. The two applications of cut encode the application of two lemmas ε(n) for n ∈ {0, 1}: if there are infinitely many cells labelled n, then there are two cells labelled by the same number.

In HandyLK , we start the specification of the proof by giving an identifier, here we choose the name the-proof: define proof the-proof Next, the end-sequent is fixed: proves A :-ex p ex q ( not p = q and f(p) = f(q) ); Now, we begin by specifying the inferences from the bottom up. In HandyLK , only the active formulas of a rule have to be specified, and no structural rules (except cut) have to be written down explicitly. The HLK compiler keeps track of the formulas used in the proof, and automatically inserts the structural rules necessary to be able to apply the rules specified by the user. The first inference in ϕ is a cut, which is a binary rule. Due to the linear nature of the HandyLK language, one of the subproofs above the binary rule has to be referenced. The following proof reference clauses are available: by proof proof auto propositional sequent explicit axiom sequent

The first clause gives the name of the subproof with which to continue, the second clause states that the subproof ends in a propositional tautology whose proof should be computed automatically, and the last clause asserts that the subproof consists solely of an axiom. In our example we reference the proof ε(1).

with cut I(1)

right by proof \epsilon(1);

This specifies an application of cut with cut formula I(1), where the right subproof will be ε(1). In LKDe, this will be a rule application

Γ ∆, I(1)(ε(1)) I(1), Π Λ Γ, Π ∆, Λ cut

where Γ, Π, ∆, Λ will be populated by the appropriate formulas automatically by the HLK compiler. We continue the HandyLK specification of this proof part with the left subproof of the first application of cut by encoding the second application: here, we reference both the left subproof τ and the right subproof ε(0).

with cut I(0)

left by proof \tau right by proof \epsilon(0); ;

This completes the HandyLK specification of ϕ -but to be able to actually compile the proof into an LKDe-proof, the subproofs τ, ε(0) and ε(1) have to be encoded in HandyLK . We continue by showing the HandyLK rule applications in τ, which are definition introduction and quantifier rules. The proof τ starts by expanding the two occurrences of the defined predicate I:

A ∀n∃k f (n + k) = 0, ∀n∃k f (n + k) = 1 A I(0), ∀n∃k f (n + k) = 1 def I : r A I(0), I(1) def I : r

In HandyLK , it suffices to specify the predicate to be expanded and give the auxiliary formulas of the rules, the correct main formula is then found by HLK through matching:

with undef I :-all n ex k f( n + k ) = 0, all n ex k f( n + k ) = 1;

Next, the two strong quantifiers are eliminated by ∀ : r rules, introducing the eigenvariables n 0 and n 1 :

A ∃k f (n 0 + k) = 0, ∃k f (n 1 + k) = 1 A ∃k f (n 0 + k) = 0, ∀n∃k f (n + k) = 1 ∀ : r A ∀n∃k f (n + k) = 0, ∀n∃k f (n + k) = 1 ∀ : r

The corresponding HandyLK code is with all right :-ex k f( n_0 + k ) = 0, ex k f( n_1 + k ) = 1;

Again, it suffices to specify the auxiliary formulas, the correct main formulas are found by matching. The same holds for the weak quantifier rules. In our example, we instantiate them by n 1 and n 0 , respectively:

A f (n 0 + n 1 ) = 0, f (n 1 + n 0 ) = 1 A ∃k f (n 0 + k) = 0, f (n 1 + n 0 ) = 1 ∃ : r A ∃k f (n 0 + k) = 0, ∃k f (n 1 + k) = 1 ∃ : r with ex right :-f( n_0 + n_1 ) = 0, f( n_1 + n_0 ) = 1;

Of course, HLK checks whether the quantifier rule applications are legal. Our proof τ is nearly doneit remains to decompose our assumption A and to use the commutativity of +. We only show the latter, which is encoded with an application of paramodulation:

n 0 + n 1 = n 1 + n 0 f (n 1 + n 0 ) = 1 f (n 1 + n 0 ) = 1 f (n 0 + n 1 ) = 1 f (n 1 + n 0 ) = 1 = : l 2

Such a paramodulation application is common when formalizing proofs from mathematics: an equality axiom from the background theory is used as the active equation. For this reason, it receives special treatment in HandyLK : the active equation is simply specified in a by clause.

with paramod by n_0 + n_1 = n_1 + n_0 right f( n_1 + n_0 ) = 1 :-;

This rule application can also be encoded in the general syntax for binary rules, using a proof reference:

with paramod f( n_1 + n_0 ) = 1 :left explicit axiom :-n_0 + n_1 = n_1 + n_0 ;

Recall that the definition of ϕ in HandyLK contained references to proofs ε(0) and ε(1), which show that under the assumption that there are infinitely many cells labelled 0 and 1, respectively, it follows that two cells are labelled by the same number. Clearly, these proofs have a similar structure -this fact can be exploited in HandyLK by writing a meta proof that can be instantiated with some specific terms:

define proof \epsilon with meta term i of type nat; proves I(i) :-ex p ex q ( not p = q and f(p) = f(q) );

We omit the details of the specification of the meta proof ε(i). Additionally, HandyLK supports the definition of proofs in a recursive way, which is a convenient way to encode sequences of proofs. This feature was used to encode a sequence of proofs for the formula scheme from [3].

XML format for proofs

The programs in the CERES system do not work directly with proofs written in HandyLK -these proofs are compiled into a flexible XML format using the HLK compiler. XML is a well known data representation language which allows the use of arbitrary and well known utilities for editing, transformation and presentation and standardized programming libraries. We are interested in tree-style proofs, formulas and terms. Data is structured in trees in XML, therefore the encoding and decoding of these objects is very straightforward. The format is flexible in the sense that it only assumes that proofs are trees or directed acyclic graphs of rule applications that are labelled by sequents. In our practice, it has been used successfully to encode LKDe and resolution proofs. The following abbreviated XML code represents the proof ϕ: <proof symbol="the-proof" calculus="LK"> <rule symbol="c:r" type="contrr" param="2"> <sequent>...</sequent> <rule symbol="cut" type="cut"> <sequent>...</sequent> <rule symbol="\pi:r" type="permr" param="(1 2)"> <sequent>...</sequent> <rule symbol="cut" type="cut"> <sequent>...</sequent> <prooflink symbol="\tau"/> <prooflink symbol="\epsilon(0)"/> </rule> </rule> <prooflink symbol="\epsilon(1)"/> </rule> </rule> </proof>

The symbol attributes are used for the visual presentation of the proof trees: they allow the user to identify proofs and rules. The param attributes contain additional rule information, in the example they specify which formulas are to be contracted (by the contraction rule c:r) and how the formulas are to be permuted (by the permutation rule \pi:r). The prooflink tags reference other proofs by their name and allow the representation of proofs as DAGs.

In the above example, the formulas contained in the sequents have been left out. To give an example of how a formula is encoded in the XML format, consider the following XML code corresponding to the formula R(c, f (c)) ∧ P(c): <conjunctiveformula type="and"> <constantatomformula symbol="R"> <constant symbol="c"/> <function symbol="f"> <constant symbol="c"/> </function> </constantatomformula> <constantatomformula symbol="P"> <constant symbol="c"/> </constantatomformula> </conjunctiveformula> Data is organized in our XML format in a proofdatabase containing a number of proofs. The proofdatabase may also contain 1. a list of defined predicates and their definitions, 2. a list of sequents specifying the axioms of the background theory in which the proofs are written, 3. arbitrary lists of sequents identified by some symbol (e.g. to store a Herbrand sequent).

The CERES method

To prepare for the following section, we will now introduce the theoretical background for the CERES method of cut-elimination, which is used by the CERES system to compute a proof in atomic cut normal form and, in the end, a Herbrand sequent.

The central idea of CERES consists in extracting a so-called characteristic clause set from a proof, and then using a resolution refutation of this set to obtain a proof with only atomic cuts. We consider the proofs in LKDe as directed trees with nodes which are labelled by sequents, where the root is labelled by the end-sequent. According to the inference rules, we distinguish binary and unary nodes. In an inference

ν 1 : S 1 ν 2 : S 2 ν : S x

where ν is labelled by S, ν 1 by S 1 and ν 2 by S 2 , we call ν 1 , ν 2 predecessors of ν. Similarly ν is predecessor of ν in a unary rule if ν labels the premiss and ν the consequent. Then the predecessor relation is defined as the reflexive and transitive closure of the relation above. Every node is predecessor of the root, and the axioms have only themselves as predecessors. For a formal definition of the concepts we refer to [4] and [5]. Let Ω be the set of all occurrences of cut-formulas in sequents of an LKDe-proof ϕ. The cut-formulas are not ancestors of the formulas in the end-sequent, but they might have ancestors in the axioms (if the cuts are not generated by weakening only). The construction of the characteristic clause set is based on the ancestors of the cuts in the axioms. Note that clauses are just defined as atomic sequents. We define a set of clauses C ν for every node ν in ϕ inductively:

• If ν is an occurrence of an axiom sequent S(ν), and S is the subsequent of S(ν) containing only the ancestors of Ω then C ν = {S }.

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

• Let ν 1 , ν 2 be the predecessors of ν in a binary inference. We distinguish two cases (a) The auxiliary formulas of ν 1 , ν 2 are ancestors of Ω. Then

C ν = C ν 1 ∪ C ν 2 .

(b) The auxiliary formulas of ν 1 , ν 2 are not ancestors of Ω. Then

C ν = C ν 1 × C ν 2 .

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

Theorem 1. Let ϕ be a proof in LKDe. Then the clause set CL(ϕ) is equationally unsatisfiable.

Remark. A clause set C is equationally unsatisfiable if C does not have a model where = is interpreted as equality over a domain.

Proof. This proof first appeared in [1]. Let ν be a node in ϕ and S (ν) the subsequent of S(ν) which consists of the ancestors of Ω (i.e. of a cut). It is shown by induction that S (ν) is LKDe-derivable from C ν . If ν 0 is the root then, clearly, S (ν 0 ) = and the empty sequent is LKDe-derivable from the axiom set C ν 0 , which is just CL(ϕ). As all inferences in LKDe are sound over equational interpretations (where new symbols introduced by definition introduction have to be interpreted according to the defining equivalence), CL(ϕ) is equationally unsatisfiable. Note that, without the rules = : l and = : r, the set CL(ϕ) is just unsatisfiable. Clearly the rules = : l and = : r are sound only over equational interpretations.

The next steps in CERES are

(1) the computation of the proof projections ϕ[C] w.r.t. clauses C ∈ CL(ϕ),

(2) the refutation of the set CL(ϕ), resulting in an RP-tree γ, i.e. in a deduction tree defined by the inferences of resolution and paramodulation, and

(3) "inserting" the projections ϕ[C] into the leaves of γ.

For step (1) we skip in ϕ all inferences where the auxiliary resp. main formulas are ancestors of a cut. Instead of the end-sequent S we get S •C for a C ∈ CL(ϕ).

Step (2) consists in ordinary theorem proving by resolution and paramodulation (which is equationally complete). For refuting CL(ϕ) any first-order resolution prover can be used. By the completeness of the methods we find a refutation tree γ as CL(ϕ) is unsatisfiable by Theorem 1.

Step (3) makes use of the fact that, after computation of the simultaneous most general unifier of the inferences in γ, the resulting tree γ is actually a derivation in LKDe. Indeed, after computation of the simultaneous unifier, paramodulation becomes = : l and = : r and resolution becomes cut in LKDe. Note that the definition rules, like the logical rules, do not appear in γ . Now for every leaf ν in γ , which is labelled by a clause C (an instance of a clause C ∈ CL(ϕ)) we insert the proof projection ϕ[C ]. The result is a proof with only atomic cuts.

The proof projection is only sound if the proof ϕ is skolemized, i.e. there are no strong quantifiers (i.e. quantifiers with eigenvariable conditions) in the end-sequent. If ϕ is not skolemized a priori it can be transformed into a skolemized proof ϕ in polynomial (at most quadratic) time; for details see [3].

For illustration, consider the following example:

ϕ = ϕ 1 ϕ 2 (∀x)(P(x) → Q(x)) (∃y)(P(a) → Q(y)) cut ϕ 1 = P(u) P(u) Q(u) Q(u) P(u) , P(u) → Q(u) Q(u) →: l P(u) → Q(u) (P(u) → Q(u)) →: r P(u) → Q(u) (∃y)(P(u) → Q(y)) ∃ : r(P(a) P(u) Q(u) Q(a) R Q(v) R

does the job of refuting CL(ϕ). By applying the most general unifier σ of δ , we obtain a ground refutation γ = δ σ :

P(a) P(a) Q(a) Q(a) R Q(a) R

This will serve as a skeleton for a proof in ACNF. To complete the construction, we combine the skeleton with the following projections (grounded by σ ):

Cut-elimination, proof visualization and Herbrand sequent extraction with CERES

After compiling the HandyLK source to XML with HLK, it is possible to perform proof analysis using the CERES tool. In our example, we are interested in extracting a Herbrand sequent from a cut-free proof of the end-sequent of ϕ. To this end, the CERES method is used, which extracts an unsatisfiable set of clauses from the proof and refutes it. In theory, any resolution prover can be used to refute this set of clauses; Table 1 lists the format conversions currently supported by our implementation. In our example, we use Otter to find a resolution refutation. Running CERES yields the following characteristic clause set in Otter input format -> =("f"(+(x4, x5)), "0"), =("f"(+(x5, x4)), "1"). % (C1) =("f"(+(x4, x6)), "0"), =("f"(+(+(+(x4, x6), "1"), x7)), "0") ->. % (C2) =("f"(+(x4, x6)), "1"), =("f"(+(+(+(x4, x6), "1"), x7)), "1") ->. % (C3) which corresponds to the set of clauses

CL(π) = { f (x 4 + x 5 ) = 0, f (x 5 + x 4 ) = 1; f (x 4 + x 6 ) = 0, f (((x 4 + x 6 ) + 1) + x 7 ) = 0 ; f (x 4 + x 6 ) = 1, f (((x 4 + x 6 ) + 1) + x 7 ) = 1 } which is refutable in arithmetic.

The Otter proof object resulting from the successful refutation is then converted into a resolution tree in XML format. According to the CERES method, this refutation is then transformed into an LKDe proof ϕ of the end-sequent of ϕ in ACNF. ϕ consists of 1262 rules, and is clearly too large to be depicted here (a small part of it can be seen in Figure 2(b)). From ϕ , a Herbrand sequent is extracted and stored in XML as a list of sequents (containing only the Herbrand sequent). All proofs and sequents computed during the analysis can be visualized using ProofTool as seen in Figure 2. To make the Herbrand sequent extracted in our example easier to read, the terms have been simplified modulo commutativity and associativity of +, and the following abbreviations are used:

p 1 = x + z + 2, p 2 = x + z + 4, p 3 = z + 1, p 4 = x + y + z + 3, p 5 = w + x + y + z + 6, p 6 = w + x + y + z + 8, p 7 = w + x + y + z + 4,

With this, the Herbrand sequent of the ACNF of the tape proof is

f (p 1 ) = 0 ∨ f (p 1 ) = 1, f (p 2 ) = 0 ∨ f (p 2 ) = 1, f (p 3 ) = 0 ∨ f (p 3 ) = 1, f (p 4 ) = 0 ∨ f (p 4 ) = 1, f (p 5 ) = 0 ∨ f (p 5 ) = 1, f (p 6 ) = 0 ∨ f (p 6 ) = 1, f (p 7 ) = 0 ∨ f (p 7 ) = 1 p 1 = p 2 ∧ f (p 1 ) = f (p 2 ), p 3 = p 1 ∧ f (p 3 ) = f (p 1 ), p 3 = p 2 ∧ f (p 3 ) = f (p 2 ), p 1 = p 4 ∧ f (p 1 ) = f (p 4 ), p 5 = p 6 ∧ f (p 5 ) = f (p 6 ), p 7 = p 5 ∧ f (p 7 ) = f (p 5 ), p 7 = p 6 ∧ f (p 7 ) = f (p 6 ), p 4 = p 7 ∧ f (p 4 ) = f (p 7 ).

Clearly, the Herbrand sequent is much smaller than the ACNF from which it is extracted. As it contains all quantifier instantiation information from the proof, it is much better suited to human interpretation than the proof itself. The Herbrand sequent we extracted from ϕ can be interpreted as the following proof:

Theorem 2. On a tape with infinitely many cells where each cell is labelled 0 or 1, there are two distinct cells that are labelled the same.

Proof. It is easy to see that the following inequalities hold:

p 1 = p 2 , p 3 = p 1 , p 3 = p 2 , p 1 = p 4 , p 5 = p 6 , p 7 = p 5 , p 7 = p 6 , p 4 = p 7 .

We may therefore delete their occurrences from the right side of the Herbrand sequent and obtain the simplified sequent Now, we assume that this sequent is false and obtain a contradiction. If the sequent is false, then all formulas on the left side are true and all formulas on the right side are false, so we may assume f (p i ) = 0 ∨ f (p i ) = 1 for i ∈ {1, . . . , 7}. Let f (p 1 ) = a with a ∈ {0, 1} and let ā = 1 − a. We have assumed that the first formula on the right side is false, so f (p 2 ) = ā. From the second formula we obtain f (p 3 ) = ā, and from the third f (p 3 ) = ā = a, which yields the desired contradiction.

f (p 1 ) = 0 ∨ f (p 1 ) = 1, f (p 2 ) = 0 ∨ f (p 2 ) = 1, f (p 3 ) = 0 ∨ f (p 3 ) = 1, f (p 4 ) = 0 ∨ f (p 4 ) = 1, f (p 5 ) = 0 ∨ f (p 5 ) = 1, f (p 6 ) = 0 ∨ f (p 6 ) = 1, f (p 7 ) = 0 ∨ f (p 7 ) = 1 f (p 1 ) = f

Note that the proof extracted from the Herbrand sequent uses only 3 cells even though the sequent itself is not minimal. Still, the proof yields a minimal Herbrand sequent directly: Comparing the proof obtained from the Herbrand sequent with the original proof, we have gained an important piece of information: in the original proof, it is shown that either infinitely many cells are labelled 0 or 1, while in the cut-free proof, only finitely many cells are used in the proof.

Open problems and future work

On the theoretical side we are working on the following two major extensions of the CERES-method: The first is an extension of CERES to second-order logic, a first step in that direction has been achieved by extending it to the fragment of second-order proofs defined by containing only quantifier-free comprehension in [9]. This extension will allow the formalization of a much broader range of mathematical proofs and yield a more convenient proof formalization. The second theoretical extension enables the method to work without skolemization whose main benefit will be the ability to eliminate single cuts or even parts of a cut which is more realistic in mathematical applications than the simultaneous elimination of all cuts.

Concerning the practical aspects, it became clear in our experiments with the system that there are two bottlenecks: 1. the formalization of the input proof and 2. finding a resolution refutation of the characteristic clause set. Accordingly also these two points are of major concern for our future work.

To ease the formalization of the input proof, we plan to enhance the capabilities of HLK, in particular those of the auto propositional-mode to cover also reasoning in equational background theories