=Paper=
{{Paper
|id=Vol-378/paper-2
|storemode=property
|title=Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions
|pdfUrl=https://ceur-ws.org/Vol-378/paper2.pdf
|volume=Vol-378
}}
==Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions==
https://ceur-ws.org/Vol-378/paper2.pdf
Proof Analysis with HLK, CERES and ProofTool:
Current Status and Future Directions
Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
Vienna University of Technology
Vienna, Austria
Abstract
CERES, HLK and ProofTool form together a system for the computer-aided analysis of mathe-
matical proofs. This analysis is based on a proof transformation known as cut-elimination, which
corresponds to the elimination of lemmas in the corresponding informal proofs. Consequently, the
resulting formal proof in atomic-cut normal form corresponds to a direct, i.e. without lemmas, infor-
mal mathematical proof of the given theorem.
In this paper, we firstly describe the current status of the whole system from the point of view of its
usage. Subsequently, we discuss each component in more detail, briefly explaining the formal calculi
(LK and LKDe) used, the intermediary language HandyLK, the CERES method of cut-elimination
by resolution and the extraction of Herbrand sequents. Three successful cases of application of the
system to mathematical proofs are then summarized. And finally we discuss extensions of the system
that are currently under development or that are planned for the short-term future.
1 Introduction
Proof synthesis and analysis form the very core of mathematical activity. While the application of au-
tomated reasoning techniques to proof synthesis is the focus of large research fields such as automated
theorem proving and interactive theorem proving, the corresponding use of automated reasoning tech-
niques in proof analysis has received considerably less attention. Nevertheless, the importance of proof
analysis to mathematics should not be underestimated. Indeed, many mathematical concepts such as
the notion of group or the notion of probability were introduced by analyzing existing mathematical
arguments [Pol54a, Pol54b].
CERES, HLK and ProofTool are three computer programs that form a system for the computer-aided
analysis of mathematical proofs. HLK is responsible for the formalization of mathematical proofs; CERES
is responsible for transformations of formal proofs and for the extraction of relevant information from
them; and ProofTool is responsible for the visualization of formal proofs.
The most useful proof transformation implemented by CERES for the purpose of proof analysis is
cut-elimination. The elimination of cuts from the formalized proofs corresponds to the elimination of
lemmas from the original informal proofs. By interpreting the resulting (cut-free or in atomic-cut normal
form) proof, a mathematician can obtain a new direct informal proof of the theorem under consideration.
The elimination performed by CERES follows the CERES method [BL00], which relies on the resolution
calculus and is essentially different from reductive methods such as the first algorithm for cut-elimination
introduced by Gentzen [Gen69]. On the other hand, for the extraction and storage of relevant information
from proofs, CERES currently uses the ideas of characteristic clause set and Herbrand sequent.
In this paper we start with an overview of the system, followed by a discussion of some details
of each of the three component programs. Three successful cases of application of the system to real
mathematical proofs are then summarized. And finally, we present our plans for the further development
and extension of the system.
Sutcliffe G., Colton S., Schulz S. (eds.); Proceedings of ESARM 2008, pp. 23-41
23
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
2 Overview of the Architecture and Workflow
Figure 1 sketches how HLK, CERES and ProofTool can be used by a mathematician to analyze existing
mathematical proofs and obtain new ones.
Figure 1: Working with HLK, CERES and ProofTool.
According to the labels in the edges of Figure 1, the following steps are executed within the system and
in interaction with the user:
1. The user (usually a mathematician) selects an interesting informal mathematical proof to be trans-
formed 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, an intermediary language between natural mathe-
matical language and formal calculi.
3. The proof written in HandyLK is input to HLK, the compiler of HandyLK.
4. HLK generates a formal proof in sequent calculus LKDe.
5. The formal proof is input to CERES, which is responsible for cut-elimination and various other
proof-transformations that serve as pre- and post-processing, such as proof skolemization, upward
shifting of equality rules and Herbrand sequent extraction.
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. Otter1 or Prover92 .
1 Otter Website: http://www-unix.mcs.anl.gov/AR/otter/
2 Prover9 Website: http://www.cs.unm.edu/ mccune/prover9/
24
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
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 atomic-
cut 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 that summarizes
the creative content of the ACNF is extracted and output as well.
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.
2.1 Implementation
HLK3 , CERES4 and ProofTool5 are free and open-source programs written in ANSI-C++ (the C++ Pro-
gramming Language following the International Standard 14882:1998 approved as an American National
Standard), and they are therefore likely to run on all operating systems. However, at this time only Linux
and Mac OS X are supported. Nevertheless, to make it easier for the system to be used also by users of
unsupported operating systems or even by users of Linux and Mac OS X who are not so familiar with
software development, a virtual machine containing the whole system pre-installed is also available for
download.
CERES and ProofTool use XML files satisfying the proofdatabase DTD6 for the storage of formal
logical structures (e.g. the original proof, the ACNF, the projections, the Herbrand sequent).
3 HLK for Proof Formalization
In order to analyze mathematical proofs in an automated way, we must firstly write down the proof
according to the rules of a formal logical calculus, so that the formalized proofs are then well-defined
data-structures, suitable to be manipulated automatically by computers. On the one hand, these data
structures should be as simple as possible, to allow theoretical logical investigations as well as the easy
implementation of algorithms. On the other hand, they should be as rich and close to the natural language
of informal mathematical proofs as possible. Therefore, the chosen formal calculus should optimize a
trade-off between simplicity and richness of the data structures.
With this in mind, the sequent calculus LK was the initial choice. It is a very well-known and well-
studied logical calculus, for which proof-theoretical results abound. The specific variant that we use
is detailed in Subsection 3.1. To bring it closer to the natural language of informal mathematics, we
extended it with definition and equality rules. The resulting calculus is called LKDe and its details are
discussed in Subsections 3.2 and 3.3.
3 HLK Website: http://www.logic.at/hlk
4 CERES Website: http://www.logic.at/ceres
5 ProofTool Website: http://www.logic.at/prooftool
6 ProofDatabase DTD: http://www.logic.at/ceres/xml/4.0/proofdatabase.dtd
25
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
However, LKDe is still uncomfortable to be used directly to write proofs down, because its data
structures for proofs are nested and contain many repetitions of formulas in the context of ancestor
sequents. To solve this problem HandyLK was created to serve as an intermediary language, as explained
in detail in Subsection 3.4.
3.1 The Sequent Calculus LK
A sequent is a pair of sequences of formulas. The sequence in the left side of the sequent is called its
antecedent; and the sequence in the right is its succedent. A sequent can be interpreted as the statement
that at least one of the formulas in the succedent can be proved from the formulas in the antecedent. A
sequent calculus proof or derivation is a tree where the leaf-nodes are axiom sequents and the edges are
inferences according to the inference rules of the sequent calculus. Axiom sequents are arbitrary atomic
sequents specified by a background theory (e.g. the reflexivity axiom scheme ` t = t for all terms t,
expressing the reflexivity of equality) or tautological atomic sequents (i.e. A ` A).
There are many sequent calculi. Our variant uses the following rules:
• Propositional-rules:
Γ ` ∆, A Π ` Λ, B A, Γ ` ∆ A, Γ ` ∆
∧:r ∧ : l1 ∧ : l2
Γ, Π ` ∆, Λ, A ∧ B A ∧ B, Γ ` ∆ B ∧ A, Γ ` ∆
A, Γ ` ∆ B, Π ` Λ Γ ` ∆, A Γ ` ∆, A
∨:l ∨ : r1 ∨ : r2
A ∨ B, Γ, Π ` ∆, Λ Γ ` ∆, A ∨ B Γ ` ∆, B ∨ A
Γ ` ∆, A B, Π ` Λ A, Γ ` ∆, B
→: l →: r
A → B, Γ, Π ` ∆, Λ Γ ` ∆, A → B
A, Γ ` ∆ Γ ` ∆, A
¬:r ¬:l
Γ ` ∆, ¬A ¬A, Γ ` ∆
In the rules ∧ : l1,∧ : l2,∨ : r1,∨ : r2, we say that the formula B is a weak subformula of A.
• Quantifier-rules:
Γ ` ∆, A{x ← α} A{x ← t}, Γ ` ∆
∀:r ∀:l
Γ ` ∆, (∀x)A (∀x)A, Γ ` ∆
Γ ` ∆, A{x ← t} A{x ← α}, Γ ` ∆
∃:r ∃:l
Γ ` ∆, (∃x)A (∃x)A, Γ ` ∆
For the ∀ : r and the ∃ : l rules, the eigenvariable condition must hold: α can occur neither in Γ
nor in ∆ nor in A. For the ∀ : l and the ∃ : r rules the term t must not contain a variable that is bound
in A.
• Weakening-rules:
Γ`∆ w:r Γ`∆
w:l
Γ ` ∆, A1 , . . . , An A1 , . . . , An , Γ ` ∆
where n > 0
• Contraction-rules:
(m ) (m ) (m ) (m )
Γ ` A1 1 , . . . , An n A1 1 , . . . , An n ` ∆
c(m1 , . . . , mn ) : r c(m1 , . . . , mn ) : l
Γ ` A1 , . . . , An A1 , . . . , An ` ∆
where mi > 0 for 1 ≤ i ≤ n and A(k) denotes k copies of A.
26
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
• Permutation-rules:
A1 , . . . , An ` ∆ Γ ` A1 , . . . , An
π(σ ) : l π(σ ) : r
B1 , . . . , Bn ` ∆ Γ ` B1 , . . . , Bn
where σ is a permutation which is interpreted as a function specifying bottom-up index mapping,
i.e. Bi = Aσ (i) .
• Cut-rule:
Γ ` ∆, A A, Π ` Λ
cut
Γ, Π ` ∆, Λ
3.2 The Sequent Calculus LKe
Equality is widely used in real mathematical proofs. Carrying the axioms of equality along the proof
within the antecedent of the sequents would render large, redundant and unreadable proofs. Therefore,
LK was extended in [BHL+ 06] to LKe with the following rules:
• Equality-rules:
Γ ` ∆, s = t Π ` Λ, A[s]Ξ Γ ` ∆, s = t A[s]Ξ , Π ` Λ
= (Ξ) : r1 = (Ξ) : l1
Γ, Π ` ∆, Λ, A[t]Ξ A[t]Ξ , Γ, Π ` ∆, Λ
Γ ` ∆,t = s Π ` Λ, A[s]Ξ Γ ` ∆,t = s A[s]Ξ , Π ` Λ
= (Ξ) : r2 = (Ξ) : l2
Γ, Π ` ∆, Λ, A[t]Ξ A[t]Ξ , Γ, Π ` ∆, Λ
where Ξ is a set of positions in A and s and t do not contain variables that are bound in A.
3.3 The Sequent Calculus LKDe
Definition introduction is a simple and very powerful tool in mathematical practice, allowing the easy
introduction of important concepts and notations (e.g. groups, lattices, . . . ) by the introduction of new
symbols. Therefore, LKe was extended in [BHL+ 06] to LKDe with the following rules:
• Definition-rules: They correspond directly to the extension principle in predicate logic and in-
troduce new predicate and function symbols as abbreviations for formulas and terms. 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 ), Γ ` ∆ Γ ` ∆, A(t1 , . . . ,tk )
d:l d:r
P(t1 , . . . ,tk ), Γ ` ∆ Γ ` ∆, P(t1 , . . . ,tk )
for arbitrary sequences of terms t1 , . . . ,tk .
3.4 HandyLK
In this subsection, we will focus on some particular features of HandyLK ’s syntax7 . These features make
it more comfortable to write down proofs in HandyLK and then automatically translate them with HLK
to LKDe instead of writing them directly and manually in LKDe.
When typing proofs in a naive notation for LKDe (e.g. a LISP-like notation for tree structures), two
problems are encountered. Firstly, one would have to repeat many formulas that are not changed by the
application of inference rules, i.e. those formulas that occur in the contexts Γ, ∆, Π and Λ and are simply
carried over from the premises to the conclusions. Secondly, large branching proofs quickly become
7 HandyLK full syntax specification: http://www.logic.at/hlk/handy-syntax.pdf
27
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
unreadable due to the nesting of subproofs within subproofs. The partial HandyLK code below shows
how the first problem is avoided in the system’s intermediary language for proof formalization.
define proof \varphi 1
proves
all x ( not P(x) or Q(x) ) :− all x ex y ( not P(x) or Q(y) );
with all right
:− ex y ( not P(\alpha) or Q(y) );
with all left
not P(\alpha) or Q(\alpha) :− ;
with ex right
:− not P(\alpha) or Q(\alpha);
continued auto propositional
not P(\alpha) or Q(\alpha) :− not P(\alpha) or Q(\alpha);
;
The code above starts by declaring a proof and the end-sequent that it derives. Then it lists the rules
that have to be applied successively to the end-sequent in a bottom up way. For each inference, only the
auxiliary formulas have to be specified. Context formulas are handled automatically by HLK.
Another useful feature shown above is the HandyLK command “continued auto propositional”. It
specifies that the current sequent can be derived from tautological axioms by application of propositional
rules. In such cases, HLK is able to produce the proof automatically.
For the example above, HLK generates the following LKDe proof:
ϕ1 :=
P(α) ` P(α)
¬:r
` P(α), ¬P(α)
¬:l
¬P(α) ` ¬P(α) Q(α) ` Q(α)
∨ : r1 ∨ : r2
¬P(α) ` ¬P(α) ∨ Q(α) Q(α) ` ¬P(α) ∨ Q(α)
∨:l
¬P(α) ∨ Q(α) ` ¬P(α) ∨ Q(α), ¬P(α) ∨ Q(α)
c:r
¬P(α) ∨ Q(α) ` ¬P(α) ∨ Q(α)
∃:r
¬P(α) ∨ Q(α) ` (∃y)(¬P(α) ∨ Q(y))
∀:l
(∀x)(¬P(x) ∨ Q(x)) ` (∃y)(¬P(α) ∨ Q(y))
∀:r
(∀x)(¬P(x) ∨ Q(x)) ` (∀x)(∃y)(¬P(x) ∨ Q(y))
The other code below shows how HandyLK avoids the problem of nesting and branching. A premise
of any inference can have a link to another proof instead of having the auxiliary subsequent of that
premise (in the example below, the left branch has a link to the subproof ϕ1 and the right branch, a link
to ϕ2 ). Hence, large subproofs can be specified somewhere else in the file, instead of appearing nested
inside the proof.
define proof \varphi
proves
P(a), all x ( not P(x) or Q(x) ) :− ex y Q(y);
with cut all x ex y ( not P(x) or Q(y) )
left by proof \varphi 1
right by proof \varphi 2;
;
28
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
Finally it should be noted that HandyLK allows parameterizing meta-terms and meta-formulas in
proofs. Hence it is thus capable of expressing recursive definitions of proof schemata, enabling the
user to define infinite proof sequences8 . In the code below, for example, a recursive proof is defined,
parameterized by the meta-term n. The proof at level n can refer to the proof at level n − 1, pr[n − 1], in
the same way that the recursive function f r at level n, f r[n], refers to f r[n − 1].
define function f of type nat to nat;
define recursive function fr( x ) to nat
at level 0 by x
at level n by f( fr[n - 1](x) )
;
define recursive proof pr
at level 0 proves
P(a) :- P( fr[0](a) );
...
at level n proves
P(a), all x ( P(x) impl P( f(x) ) ) :- P( fr[n](a) );
...
;
HLK can output the LKDe proof either as a LATEX file or as an XML file satisfying to the proofdatabase
DTD.
4 CERES
After the proof has been formalized in LKDe with HLK, it can be transformed with the CERES system.
Among the transformations that can be performed by CERES the most interesting one is cut-elimination,
which produces a proof in atomic-cut normal form. The ACNF is mathematically interesting, because
cut-elimination in formal proofs corresponds to the elimination of lemmas in informal proofs. Hence the
ACNF corresponds to an informal mathematical proof that is analytic in the sense that it does not use
auxiliary notions that are not already explicit in the theorem itself.
To perform cut-elimination, CERES uses a method that employs the resolution calculus to eliminate
cuts in a global way, instead of the more traditional local reductive methods [Gen69]. The CERES
method has been described in various degrees of detail and with different emphasis in [BL00, BHL+ 05,
BHL+ 06, BHL+ ] and hence it is just sketched in Subsection 4.1.
Although the ACNF is mathematically interesting, it is too large and full of redundant information.
Its direct analysis and interpretation by humans is therefore too difficult. To overcome this, an algorithm
to extract the essential information of proofs has been recently implemented within CERES. It performs
Herbrand sequent extraction and is sketched in Subsection 4.2.
8 The Exponential Proofs (http://www.logic.at/ceres/examples/index.html) are a good example of HandyLK being used to define
infinite proof sequences with parameterized meta-terms and meta-formulas
29
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
4.1 The CERES Method
The CERES method transforms any LKDe-proof with cuts into an atomic-cut normal form (ACNF)
containing no non-atomic cuts. The remaining atomic cuts are, generally, non-eliminable, because LKDe
admits non-tautological axiom sequents.
The transformation to ACNF via Cut-Elimination by Resolution is done according to the following
steps:
1. Construct the (always unsatisfiable [BL00]) characteristic clause set of the original proof by col-
lecting, joining and merging sets of clauses defined by the ancestors of cut-formulas in the axiom
sequents of the proof.
2. Obtain from the characteristic clause set a grounded resolution refutation, which can be seen as
an LKe-proof by exploiting the fact that the resolution rule is essentially a cut-rule restricted to
atomic cut-formulas only and by mapping paramodulations to equality-inferences.
3. For each clause of the characteristic clause set, construct a projection of the original proof with
respect to the clause.
4. Construct the ACNF by plugging the projections into the corresponding clauses in the leaves of
the grounded resolution refutation tree (seen as an LKe-proof) and by adjusting the resulting proof
with structural inferences (weakening, contractions and permutations) if necessary. Since the pro-
jections do not contain cuts and the refutation contains atomic cuts only, the resulting LKDe proof
will indeed be in atomic-cut normal form.
Theoretical comparisons of the CERES with reductive methods can be found in [BL00, BL06]. For
illustration, consider the following example:
ϕ=
ϕ1 ϕ2
cut
(∀x)(P(x) → Q(x)) ` (∃y)(P(a) → Q(y))
ϕ1 =
P(u)? ` P(u) Q(u) ` Q(u)?
→: l
P(u)? , P(u) → Q(u) ` Q(u)?
→: r
P(u) → Q(u) ` (P(u) → Q(u))?
∃:r
P(u) → Q(u) ` (∃y)(P(u) → Q(y))?
∀:l
(∀x)(P(x) → Q(x)) ` (∃y)(P(u) → Q(y))?
∀:r
(∀x)(P(x) → Q(x)) ` (∀x)(∃y)(P(x) → Q(y))?
ϕ2 =
P(a) ` P(a)? Q(v)? ` Q(v)
→: l
P(a), (P(a) → Q(v))? ` Q(v)
→: r
(P(a) → Q(v))? ` P(a) → Q(v)
∃:r
(P(a) → Q(v))? ` (∃y)(P(a) → Q(y))
∃:l
(∃y)(P(a) → Q(y))? ` (∃y)(P(a) → Q(y))
∀:l
(∀x)(∃y)(P(x) → Q(y))? ` (∃y)(P(a) → Q(y))
The crucial information extracted by CERES is the characteristic clause set, which is based on the
ancestors of the cut-formulas (marked here by ?). For this proof, the set is CL(ϕ) = {P(u) ` Q(u); `
30
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
P(a); Q(v) `}. This set is always unsatisfiable, here the resolution refutation δ of CL(ϕ)
` P(a) P(u) ` Q(u)
R
` Q(a) Q(v) `
R
`
does the job. By applying the most general unifier σ of δ , we obtain a ground refutation γ = δ σ :
` P(a) P(a) ` Q(a)
R
` Q(a) Q(a) `
R
`
This will serve as a skeleton for a proof in ACNF. To complete the construction, we have to compute the
projections to the clauses that are used in the refutation, this essentially works by leaving out inferences
on ancestors of cut-formulas and applying σ :
ϕ(C1 ) =
P(a) ` P(a) Q(a) ` Q(a)
→: l
P(a), P(a) → Q(a) ` Q(a)
∀:l
P(a), (∀x)(P(x) → Q(x)) ` Q(a)
w:r
P(a), (∀x)(P(x) → Q(x)) ` (∃y)(P(a) → Q(y)), Q(a)
ϕ(C2 ) =
P(a) ` P(a)
w:r
P(a) ` P(a), Q(v)
→: r
` P(a) → Q(v), P(a)
∃:r
` (∃y)(P(a) → Q(y)), P(a)
w:l
(∀x)(P(x) → Q(x)) ` (∃y)(P(a) → Q(y)), P(a)
ϕ(C3 ) =
Q(a) ` Q(a)
w:l
P(a), Q(a) ` Q(a)
→: r
Q(a) ` P(a) → Q(a)
∃:r
Q(a) ` (∃y)(P(a) → Q(y))
w:l
Q(a), (∀x)(P(x) → Q(x)) ` (∃y)(P(a) → Q(y))
Finally, we combine the projections and the ground refutation:
ϕ(γ) =
ϕ(C2 ) ϕ(C1 )
B ` C, P(a) P(a), B ` C, Q(a) ϕ(C3 )
cut
B, B ` C,C, Q(a) Q(a), B ` C
cut
B, B, B ` C,C,C
contractions
B`C
where B = (∀x)(P(x) → Q(x)), C = (∃y)(P(a) → Q(y)). Clearly, ϕ(γ) is a proof of the end-sequent of
ϕ in ACNF.
4.2 Herbrand Sequent Extraction
Our motivation to devise and implement Herbrand sequent extraction algorithms was the need to ana-
lyze and understand the result of proof transformations performed automatically by the CERES system,
especially the ACNF.
31
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
Definition 4.1 (Herbrand Sequents of a Sequent). Let s be a sequent without free-variables and con-
taining weak quantifiers only (i.e. universal quantifiers occur only with negative polarity and existential
quantifiers occur only with positive polarity). We denote by s0 the sequent s after removal of all its quan-
tifiers. Any propositionally valid sequent in which the antecedent (respectively, succedent) formulas are
instances (i.e. their free variables are possibly instantiated by other terms) of the antecedent (respectively,
succedent) formulas of s0 is called a Herbrand sequent of s.
Let s be an arbitrary sequent and s0 a skolemization of s. Any Herbrand sequent of s0 is a Herbrand
sequent of s.
Theorem 4.1 (Herbrand’s Theorem). A sequent s is valid if and only if there exists a Herbrand sequent
of s.
Proof. Originally in [Her30], stated for Herbrand disjunctions. Also in [Bus95] with more modern proof
calculi.
Herbrand’s theorem guarantees that we can always obtain a Herbrand sequent from a correct proof,
a possibility that was firstly exploited by Gentzen in his Mid-Sequent Theorem, which provides an algo-
rithm for the extraction of Herbrand sequents based on the downward shifting of quantifier rules. How-
ever, Gentzen’s algorithm has one strong limitation: it is applicable only to proofs with end-sequents in
prenex form. Although we could transform the end-sequents and the proofs to prenex form, this would
compromise the readability of the formulas and require additional computational effort. Prenexification
is therefore not desirable in our context, and hence, to overcome this and other limitations in Gentzen’s
algorithm, we developed and implemented another algorithm.
To extract a Herbrand sequent of the end-sequent s of an LKDe-proof ϕ without cuts containing
quantifiers, the implemented algorithm executes two transformations:
1. Ψ ([WP08]): produces a quantifier-rule-free LKeA -proof where quantified formulas are replaced
by array-formulas containing their instances.
2. Φ (definition 4.3): transforms the end-sequent of the resulting LKeA -proof into an ordinary se-
quent containing no array-formulas. The result is a Herbrand sequent of the end-sequent of the
original proof.
Definition 4.2 (Sequent Calculus LKeA ). The sequent calculus LKeA is the sequent calculus LKe ex-
tended with the following array-formation-rules:
∆, A1 , Γ1 , . . . , An , Γn , Π ` Λ Λ ` ∆, A1 , Γ1 , . . . , An , Γn , Π
hi : l hi : r
∆, hA1 , . . . , An i, Γ1 , . . . , Γn , Π ` Λ Λ ` ∆, hA1 , . . . , An i, Γ1 , . . . , Γn , Π
The intuitive idea behind the computation of Ψ(ϕ) for an LKDe-proof ϕ consists of omitting quantifier-
inferences and definition-inferences and replacing unsound contraction-inferences by array-formation-
inferences (omissions and replacements are done in a top-down way and formulas in the downward
path of a changed formula are changed accordingly). More precisely, if a quantified formula is the
main formula of a contraction, then this contraction will not be sound anymore after the omission of the
quantifier-inferences, because its auxiliary formulas will now contain different instances of the quantified
formula instead of being exact copies of the quantified formula. Hence, the unsound contraction infer-
ences are replaced by array-formation inferences, which will collect all the instances of that quantified
formula into an array formula. This idea has been formally defined in [WP08, HLWWP08]. However,
the implemented algorithm follows an equivalent recursive definition, which is more natural to imple-
ment but quite technical, preventing a clean exposition of the fundamental idea of the transformation to
LKeA .
32
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
Definition 4.3 (Φ: Expansion of Array Formulas). The mapping Φ transforms array formulas and se-
quents into first-order logic formulas and sequents. In other words, Φ eliminates h. . .i and can be defined
inductively by:
.
1. If A is a first-order logic formula, then Φ(A) = A
.
2. Φ(hA1 , . . . , An i) = Φ(A1 ), . . . , Φ(An )
.
3. If Φ(A) = A1 , . . . , An , then Φ(¬A) = ¬A1 , . . . , ¬An
.
4. If Φ(A) = A1 , . . . , An and Φ(B) = B1 , . . . , Bm , then Φ(A◦B) = A1 ◦B1 , . . . , A1 ◦Bm , . . . , An ◦B1 , . . . , An ◦
Bm , for ◦ ∈ {∧, ∨, →}
.
5. Φ(A1 , . . . , An ` B1 , . . . , Bm ) = Φ(A1 ), . . . , Φ(An ) ` Φ(B1 ), . . . , Φ(Bm )
Example 4.1. Let ϕ be the following LKDe-proof:
[ϕ 0 ]
P(0), P(0) → P(s(0)), P(s(0)) → P(s2 (0)) ` P(s2 (0))
∀:l
P(0), P(0) → P(s(0)), (∀x)(P(x) → P(s(x)) ` P(s2 (0))
∀:l
P(0), ∀x(P(x) → P(s(x)), (∀x)(P(x) → P(s(x)) ` P(s2 (0))
c:l
P(0), ∀x(P(x) → P(s(x)) ` P(s2 (0))
∧:l
P(0) ∧ (∀x)(P(x) → P(s(x)) ` P(s2 (0))
The LKDe-pseudoproof ϕc with unsound contractions, resulting from the omission of quantifier-
inferences and definition-inferences is:
[ϕ 0 ]
P(0), P(0) → P(s(0)), P(s(0)) → P(s2 (0)) ` P(s2 (0))
c∗ : l
P(0), ∇ ` P(s2 (0))
∧:l
P(0) ∧ ∇ ` P(s2 (0))
where ∇ stands for the undeterminable main formula of the unsound contraction-inference, since it
contains different auxiliary formulas.
The LKeA -proof Ψ(ϕ), after replacement of unsound contractions by array-formations, is:
[ϕ 0 ]
P(0), P(0) → P(s(0)), P(s(0)) → P(s2 (0)) ` P(s2 (0))
hi : l
P(0), P(0) → P(s(0)), P(s(0)) → P(s2 (0)) ` P(s2 (0))
∧:l
P(0) ∧ P(0) → P(s(0)), P(s(0)) → P(s2 (0)) ` P(s2 (0))
Let s be the end-sequent of Ψ(ϕ). Then Φ(s), which is a Herbrand sequent extracted from ϕ, is:
P(0) ∧ (P(0) → P(s(0))),
` P(s2 (0))
P(0) ∧ (P(s(0)) → P(s2 (0)))
33
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
4.2.1 Further Improvements of Herbrand Sequent Extraction
Preliminary tests of the implemented algorithm described above showed that the extracted Herbrand
sequent still contained information that was irrelevant for the interpretation of the ACNF to obtain a new
informal mathematical proof corresponding to the ACNF. Such irrelevant information occurred in the
form of subformulas of the Herbrand sequent that were introduced by weakening-inferences or as the
weak subformula of the main formula of some other inference. This problem was solved by omitting
the weak subformulas in the construction of Ψ(ϕ). This improvement implies that the extracted sequent
is not strictly a Herbrand sequent anymore, because its formulas are not instances of the formulas of
the original end-sequent. However, the extracted sequent is still valid and contains the desired relevant
information about the used variable instantiations in ϕ.
5 ProofTool
ProofTool is the graphical user interface that displays the original formal proof, the skolemized proof,
the characteristic clause set, the projections, the ACNF and the Herbrand sequent to the user, so that he
can analyze them and obtain a better understanding of the original proof or a new direct informal proof
for the same theorem based on the Herbrand sequent and on the ACNF. It allows the user to zoom in and
out of the proofs and to navigate to subproofs defined by proof links. Although it is mostly intended for
proof visualization, some simple forms of proof editing, e.g. formula substitution and splitting of proofs
by the creation of new proof links, are also possible.
Figure 2: ProofTool Screenshots
6 Successful Experimental Cases
In this section, we summarize three successful cases in which the system was used for the analysis of
mathematical proofs. All the examples below constitute interesting proofs for cut-elimination because
they contain mathematical concepts in the cut-formulas which do not occur in the theorems shown.
More information about each case can be found in the respective referred papers containing the detailed
analysis.
6.1 The Tape Proof
The first proof that was analyzed using CERES (in [BHL+ 05] within LK and in [BHL+ 06] within LKDe)
was originally defined in [Urb00]. This proof deals with the following situation: We are given an infinite
34
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
tape where each cell contains either ‘0’ or ‘1’. We prove that on this tape there are two cells with the
same value. The original proof goes on to show that on the tape, there are infinitely many cells containing
‘0’ or infinitely many cells containing ‘1’. From this, it follows that there are two cells having the same
value. Clearly, these lemmas are much stronger than what is actually needed to prove the theorem, and
exactly these lemmas where eliminated by the use of CERES.
By using different resolution refinements (positive and negative hyperresolution), two different reso-
lution refutations (resulting in different ACNFs) were produced. After analysis of the argument contained
in the refutations, it turns out that the refutations differ not only formally, but also in their mathematical
interpretation. This showed that for any particular proof ψ, CERES may produce several ACNFs of the
end-sequent of ψ and each of them may contain a mathematically different argument. This example
exhibited the diversity of analytic proofs that may be obtained by using CERES.
Furthermore, in [Het07], two different tape proofs with different cut-formulas were analyzed com-
paratively. It has been observed how the characteristic clause sets of each proof determine and restrict
the kinds of mathematical arguments and direct informal mathematical proofs that can be obtained from
the ACNFs of each proof. This shows the potential of CERES not only for the analysis of single proofs,
but also for the comparative analysis of different proofs of the same theorem.
6.2 The Prime Proof
In [BHL+ ], the system was used to analyze Fürstenberg’s proof of the infinity of primes. This proof uses
topological concepts in its lemmas and proves that there are infinitely many primes. A central part in the
formalization of this proof was the possibility of expressing proof schemas in HLK— here, it was used to
formalize the inductive parts of the proof (e.g. that the union of closed sets is closed). Each proof ϕ(k)
according to the proof schema ϕ expresses that there are more than k primes. The collection of all such
proofs implies that there are infinitely many primes.
The refutation and analysis of the characteristic clause set extracted by CERES led to a direct informal
proof of the infinity of primes, which corresponded to the well-known Euclid’s argument for the infinity
of primes. Thus CERES could essentially transform Fürstenberg’s proof into Euclid’s proof.
6.3 The Lattice Proof
In [HLWWP08], the usefulness of a Herbrand sequent for understanding a formal proof was demon-
strated on a simple proof from lattice theory showing that L1-lattices (semi-lattices satisfying “inverse”
laws) are L2-lattices (semi-lattices satisfying the absorption laws) by firstly showing that L1-lattices are
L3-lattices (partially-ordered sets with greatest lower bounds and least upper bounds) and then showing
that L3-lattices are L2-lattices.
The formalization of the proof with HLK resulted in a proof with 260 inferences where the concept
of L3-lattice appears, as expected, as a cut-formula in a cut-inference. The elimination of cuts with
CERES resulted in a proof in atomic-cut normal form (ACNF) containing 214 inferences and no essential
cuts. The informal proof corresponding to the ACNF would be a direct mathematical argument proving
that L1-lattices are L2-lattices. However, due to its size, the interpretation of the ACNF to extract this
informal proof is hardly possible. On the other hand, the Herbrand sequent extracted from the ACNF
contains only 6 formulas. Analyzing the Herbrand sequent alone, it was possible to obtain the desired
informal direct proof.
35
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
7 Future Directions
The development of our systems focuses on the analysis of mathematical proofs. However, it could
also be extended to other applications of the transformation and analysis of formal proofs, e.g. for the
computation of interpolants in symbolic model checking [McM03, HJMM04].
In the following subsections, we will discuss a few improvements to the system formed by CERES,
HLK and ProofTool that are currently under development or that shall be developed in the future.
7.1 The Proof Profile
The proof profile [Het07, Het08] is a refinement of the characteristic clause set which, in addition to
the logical information about the cut-formulas, incorporates also combinatorial information about the
structure of the proof. This leads to an optimization of the CERES method in the sense that atomic-
cut normal forms generated by using the profile will always be at most the size of those generated by
using the characteristic clause set, and furthermore, the profile is stronger in detecting certain kinds of
redundancies which can yield even a non-elementary speed-up with respect to an atomic-cut normal
form generated by using the characteristic clause set. Moreover, not only is the proof profile a practical
optimization but it also gives important theoretical benefits: they have been used in [HL07] to obtain new
results about the relation between simple proof transformations and cut-elimination. Therefore, CERES
will be extended to make it possible to use the proof profile instead of the characteristic clause set.
7.2 Extension to Second-order Logic
Second-order logic extends first-order logic by allowing quantification over set variables. The reasons for
considering an extension of the CERES method to second-order logic are twofold: first, the second-order
induction axiom
(∀X)(0 ∈ X ∧ (∀x)(x ∈ X → x0 ∈ X) → (∀x)x ∈ X)
enables proofs by induction to be handled on the object level, whereas induction in first-order logic
can only be handled by (non-tautological) rules or by proof schemas. This then allows the induction
component of proofs to be handled in the same way as any other formula occuring in a proof. Secondly,
a comprehension axiom scheme
(∃X)(∀x)(x ∈ X ↔ ϕ(x))
can be formulated in second-order logic, which allows one to assert the existence of sets defined by
formulas ϕ(x). Certainly, the definition of sets by formulas is a very natural mathematical operation:
consider as an example the sentence
(∃X)(∀x)(x ∈ X ↔ (∃z)2 ∗ z = x)
which asserts the existence of the set of even numbers.
Note that the second-order axioms of induction and comprehension are preferable to the correspond-
ing schemes of first-order arithmetic and set theory in this context: the goal of proof analysis by cut-
elimination is to remove certain mathematical concepts from the proof. If, however, these concepts
appear in instances of axiom schemes in the end-sequent of the proof with cuts, they will also appear
in the end-sequent of the cut-free (or ACNF) proof. In the second-order formulation, preserving the
end-sequent does not imply preserving the instances of the schemes.
As second-order logic distinguishes between set variables and individual variables, it does not suffer
from Russel’s paradox. Still, second-order arithmetic (even with restrictions on ϕ(x) in the comprehen-
sion scheme) is powerful enough to prove a large part of ordinary mathematics (see [Sim99]).
36
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
Extending CERES to second-order logic is non-trivial: In first-order logic, proof skolemization is
used as an essential technical tool to remove strong quantifier rules going into the end-sequent from the
proof. In second-order logic, the corresponding transformation can only be applied in very special cases
(we must restrict the way in which weak second-order quantifiers occur). Consider for example:
P(β , a) ` P(β , a) P(α, b) ` P(α, b)
∀:l ∀:l
(∀x)P(x, a) ` P(β , a) (∀z)P(z, b) ` P(α, b)
∀:r ∀:r
(∀x)P(x, a) ` (∀z)P(z, a) (∀z)P(z, b) ` (∀z)P(z, b)
→: l
(∀x)P(x, a), (∀z)P(z, a) → (∀z)P(z, b) ` (∀x)P(x, b) 2
∀ : l λ x.(∀z)P(z, x)
(∀x)P(x, a), (∀X)(X(a) → X(b)) ` (∀x)P(x, b)
→: r
(∀X)(X(a) → X(b)) ` (∀x)P(x, a) → (∀x)P(x, b)
Skolemization of the proof would yield
P(s2 , a) ` P(s2 , a) P(s1 , b) ` P(s1 , b)
∀:l ∀:l
(∀x)P(x, a) ` P(s2 , a) (∀z)P(z, b) ` P(s1 , b)
→: l
(∀x)P(x, a), P(s2 , a) → (∀z)P(z, b) ` P(s1 , b) 2
∀ : l λ x.(∀z)P(z, x)
(∀x)P(x, a), (∀X)(X(a) → X(b)) ` P(s1 , b)
→: r
(∀X)(X(a) → X(b)) ` (∀x)P(x, a) → P(s1 , b)
where the ∀2 : l rule application is clearly not sound. For this reason, we will investigate an extension of
the CERES method that deals with proofs that have not been skolemized.
Also, resolution in second-order logic loses some nice properties of its first-order counterpart: first-
order logic is semi-recursive and therefore we can always find a resolution refutation of the characteristic
clause set. This is not the case for second-order logic. Still, there exist implementations of higher-order
resolution provers (e.g. Leo, see [BK98]), which we plan to adapt for use with CERES in second-order
logic.
7.3 Handling Non-skolemized Proofs and Elimination of Single Cuts
As mentioned in the previous section, skolemization of proofs in second-order logic is not always pos-
sible. Also in first-order logic, it would be advantageous to be able to apply the CERES method to
non-skolemized proofs: consider, for example, a proof ϕ containing a proof ψ as a subproof. Applying
CERES to the skolemization of ψ yields an ACNF ψ 0 . It is then not possible in general to put ψ 0 in place
of ψ in ϕ: the end-sequent of ψ may contain formula occurrences that are ancestors of cut-formulas in ϕ,
and skolemization of these formulas will prevent these cuts from being applied (as the cut-formula occur-
rences have different polarities). This leads to the fact that CERES currently only supports elimination
of all cuts of a proof at once.
On the other hand, if CERES is able to handle non-skolemized proofs this immediatly gives rise to a
method to eliminate a single uppermost cut ρ in ϕ by isolating the subproof ending with ρ and applying
CERES to it.
Our experiments with applying CERES to Fürstenberg’s proof on the infinity of primes showed that
current automated theorem provers are too weak to handle the characteristic clause sets of larger proofs.
With a method for eliminating single cuts, the problem of performing cut-elimination on a proof ϕ can
then be reduced to a sequence of cut-eliminations on proofs ψi that contain only one non-atomic cut. The
characteristic clause sets of the ψi will be less complex than that of ϕ, which will enable the theorem
provers to find a refutation more easily.
37
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
The main problem that occurs when considering non-skolemized proofs with CERES are eigenvari-
able violations of the strong quantifier rules that appear in the projections. There are different ideas on
how this problem may be resolved, a promising approach is the following: we restrict the form of the
strong quantifier rules going into the end-sequent by using, instead of eigenvariables, skolem terms as
eigenterms of the rules. In the resulting ACNF, we will then have violations of the eigenterm condi-
tions of these rules by ancestors of cut-formulas. By a proof transformation (essentially reductive cut-
elimination together with certain rule permutations) we can produce a valid ACNF. Intuitively, this works
because reductive cut-elimination always shifts cuts upwards in a proof, so eventually the cut-formulas
will be cut out at the top of the proof, and can not cause eigenterm violations below.
7.4 Extension to Superdeduction Calculi
The first logical calculi followed Hilbert’s style of having few inference rules and many axiom schemas.
The next generations of calculi such as natural deduction and sequent calculi substituted some axiom
schemas by new inference rules. Formal proofs in these calculi were therefore closer to natural informal
mathematical proofs, simply because the new inference rules corresponded more closely to some kinds
of inferences that are usually done in informal mathematical argumentation. However, the new inference
rules substituted only axioms that contained purely logical information about the behavior of connec-
tives and quantifiers. Informal mathematical argumentation, on the other hand, contains many informal
inferences based on axioms containing mathematical information about a concrete domain of mathemat-
ical practice. The trend in the evolution of formal calculi for the actual formalization of mathematical
proofs is to incorporate such mathematical axioms into rules of inference, in the same way that natural
deduction and sequent calculi incorporated purely logical axioms into their rules of inference.
The use of arbitrary initial sequents, equation-rules and definition-rules in LKDe can be seen as a
small step within this trend. Another related but bigger step, though, was done with the proposal of su-
perdeduction rules[BHK07], which roughly correspond to a rigorous combination of our definition-rules
with other LK inferences in such a way that all auxiliary formulas of the superdeduction inference are
atomic. More precisely, superdeduction inferences can be easily simulated in LKDe by substituting them
by many LK inferences followed by a definition-inference. Nevertheless, proofs using superdeduction
inferences are shorter, more readable and closer to informal mathematical proofs than pure LKDe-proofs.
To support superdeduction inferences, the CERES method and CERES, HLK and
ProofTool will have to be extended to support rules of arbitrary arity, because they currently work with
unary and binary rules only and superdeduction rules can have an arbitrary number of premises.
7.5 Better Herbrand Sequents
Our algorithm for Herbrand sequent extraction currently lacks support for definition-rules, because
definition-inferences must be omitted in the transformation to LKeA . We plan to modify the algorithm,
so that it reinserts defined formulas in the extracted Herbrand sequent, in order to further improve its
readability. Better readability could also be achieved by post-processing and compressing long terms
appearing in the formulas of Herbrand sequent. Furthermore, the usage of the Herbrand sequent as a
guide for the construction of new informal direct mathematical proofs could be made easier by enriching
the Herbrand sequent with the axiom links that were used in the proof, similarly to what is done in proof
nets and atom flows.
38
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
7.6 Resolution Refinements for Cut-Elimination
The CERES method relies on a search for a refutation of the characteristic clause set. Although the
characteristic clause set is known to be always unsatisfiable, the search space with unrestricted resolution
or even with typical resolution refinements (e.g. hyper-resolution, unit-resolution, . . . ) can be so large
that theorem provers like Otter and Prover9 do not find a refutation in a reasonable time. This occurs
specially if the proof and its characteristic clause set are large or if the proof contains equality rules, in
which case the refutation needs paramodulation.
We plan to develop resolution refinements that will exploit the structure of the proofs in order to
restrict the search space and possibly even eliminate the need for search altogether.
7.7 Interactive Resolution Theorem Prover
In order to implement the planned resolution refinements, we have implemented a simple but flexible
resolution theorem prover. It was designed with a focus on easy plugability of new refinements and
on the possibility of interaction with the user. However, it supports only unrestricted resolution and
paramodulation so far. It still needs to be tested with large clause sets and other refinements have to be
implemented.
7.8 Improvements for HLK
The continued auto propositional feature of HLK is currently restricted to sequents that can be derived
from tautological axiom sequents. However, since LKDe allows arbitrary atomic axioms specified by a
background theory, it would be interesting if continued auto propositional were extended in order to
generate proofs automatically also for sequents that can be propositionally derived from any arbitrary
axioms, tautological or not.
7.9 Improvements for ProofTool
ProofTool supports global zooming and scrolling, which allow the user to navigate to different parts of
the proof and analyze the structure of the proof in different degrees of detail. However, for very large
proofs, navigating only via global zooming and scrolling has some disadvantages:
• If the user globally zooms in to see details of a part of the proof, he loses his view of whole proof.
Moreover, if he needs to analyze details of various distant regions of the proof, he has to zoom in
to one region, then zoom out and scroll to another far region, then zoom in again, and so on. This
is sometimes very impractical. A solution to this problem could be the use of a magnifying glass,
which would allow the user to locally zoom in, without losing his view of the whole proof, and to
easily change the local zoom to other regions of the proof just by moving the magnifying glass.
• Sometimes the user needs to navigate to some specific regions of the proof, but its precise locations
are not known a priori. Examples are:
– Assume that the user is looking at the root inference of the subproof at the left branch of a
binary inference. Then he might want to go to “the root inference of the subproof at the right
branch of this binary inference”.
– If the user is looking at a certain formula occurrence, he might want to go to “the inferences
that contain ancestors of this formula as their main occurrences”
39
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
In such situations, the user has to manually scroll and search for the desired regions. Ideally, this
problem could be solved by some simple yet expressive enough query language for positions in
proofs. In the short-term, keyboard shortcuts for typical queries could be implemented.
While the previous problems are mainly due to proof size, other problems arise from the existence
of bureaucracy and trivial structural information in LKDe-proofs. Many features shall be added to
ProofTool to overcome this. Unary structural inferences could be hidden; colors could be used to
highlight different interesting objects (corresponding formulas, ancestor paths, inferences, subproofs) in
the proof; and context formulas could be hidden.
Finally, ProofTool’s editing capabilities could be extended to allow simple proof transformations
to be done directly via the graphical user interface.
7.10 Alternatives for HandyLK and HLK
HandyLK is not the only language for the formalization of mathematical proofs. Other languages and
systems, such as COQ9 , Isabelle10 , Mizar11 and ForTheL12 , also aim at helping mathematicians in this
task. We would like to study the possibility of integrating these languages and systems to CERES, as
alternatives to HandyLK and HLK. We foresee two potential compatibility obstacles. On the theoretical
side, these languages and systems might not use the same logics and calculi that CERES uses. On the
implementation side, these alternatives systems must easily output a formal proof object, and this proof
object must be easily convertible to the internal data structures that CERES uses.
8 Conclusion
As summarized in Section 6, the system formed by HLK, CERES and ProofTool has been applied in the
transformation and analysis of real mathematical proofs. It constitutes therefore a successful example
of automated reasoning being employed in mathematics. In this paper, an overview of the system was
given, with a special emphasis on recently added features (e.g. Herbrand sequent extraction) and on
extensions that are currently being developed. We showed the current status of our efforts in employing
automated proof theoretical methods in mathematical analysis, and we pointed the directions that we
intend to follow in order to bring these methods even closer to mathematical practice.
9 Acknowledgements
The authors would like to thank the anonymous referees for their interesting comments and suggestions.
References
[BHK07] Paul Brauner, Clement Houtmann, and Claude Krichner. Principles of Superdeduction. In Twenty-
Second Annual IEEE Symposium on Logic in Computer Science (LiCS), 2007.
[BHL+ ] Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, and Hendrik Spohr. Ceres: An
Analysis of Fürstenberg’s Proof of the Infinity of Primes. to appear in Theoretical Computer Sci-
ence.
9 COQ Website: http://coq.inria.fr/
10 Isabelle Website: http://www.cl.cam.ac.uk/research/hvg/Isabelle/
11 Mizar Website: http://mizar.org/
12 ForTheL Website: http://nevidal.org.ua/
40
Proof Analysis with HLK, CERES and ProofTool Hetzl, Leitsch, Weller, Woltzenlogel Paleo
[BHL+ 05] Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, and Hendrik Spohr. Cut-
Elimination: Experiments with CERES. In Franz Baader and Andrei Voronkov, editors, Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR) 2004, volume 3452 of Lecture Notes
in Computer Science, pages 481–495. Springer, 2005.
[BHL+ 06] Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, and Hendrik Spohr. Proof Trans-
formation by CERES. In Jonathan M. Borwein and William M. Farmer, editors, Mathematical
Knowledge Management (MKM) 2006, volume 4108 of Lecture Notes in Artificial Intelligence,
pages 82–93. Springer, 2006.
[BK98] Christoph Benzmüller and Michael Kohlhase. Leo — A Higher-Order Theorem Prover. In Proc.
CADE-15, volume 1421, pages 139–143, Heidelberg, Germany, 1998. Springer-Verlag.
[BL00] Matthias Baaz and Alexander Leitsch. Cut-elimination and Redundancy-elimination by Resolution.
Journal of Symbolic Computation, 29(2):149–176, 2000.
[BL06] Matthias Baaz and Alexander Leitsch. Towards a clausal analysis of cut-elimination. Journal of
Symbolic Computation, 41(3–4):381–410, 2006.
[Bus95] S. R. Buss. On Herbrand’s theorem. Lecture Notes in Computer Science, 960:195, 1995.
[Gen69] G. Gentzen. Untersuchungen über das logische Schließen. In M.E.Szabo, editor, The Collected
Papers of Gerhard Gentzen, pages 68–131. North-Holland Publishing Company, Amsterdam - Lon-
don, 1969.
[Her30] J. Herbrand. Recherches sur la Theorie de la Demonstration. PhD thesis, University of Paris, 1930.
[Het07] Stefan Hetzl. Characteristic Clause Sets and Proof Transformations. PhD thesis, Vienna University
of Technology, 2007.
[Het08] Stefan Hetzl. Proof Profiles. Characteristic Clause Sets and Proof Transformations. VDM, 2008.
[HJMM04] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. Mcmillan. Abstractions from
proofs. In POPL ’04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles
of programming languages, volume 39, pages 232–244, New York, NY, USA, January 2004. ACM
Press.
[HL07] Stefan Hetzl and Alexander Leitsch. Proof Transformations and Structural Invariance. In Ste-
fano Aguzzoli, Agata Ciabattoni, Brunella Gerla, Corrado Manara, and Vincenzo Marra, editors,
Algebraic and Proof-theoretic Aspects of Non-classical Logics, volume 4460 of Lecture Notes in
Artificial Intelligence, pages 201–230. Springer, 2007.
[HLWWP08] Stefan Hetzl, Alexander Leitsch, Daniel Weller, and Bruno Woltzenlogel Paleo. Herbrand Sequent
Extraction. to appear in the proceedings of Mathematical Knowledge Management (MKM) 2008,
2008.
[McM03] K. L. McMillan. Interpolation and SAT-Based Model Checking. Lecture Notes in Computer Sci-
ence. Springer, 2003.
[Pol54a] G. Polya. Mathematics and plausible reasoning, Volume I: Induction and Analogy in Mathematics.
Princeton University Press, 1954.
[Pol54b] G. Polya. Mathematics and plausible reasoning, Volume II: Patterns of Plausible Inference. Prince-
ton University Press, 1954.
[Sim99] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Springer-Verlag, Heidelberg, Ger-
many, 1999.
[Urb00] Christian Urban. Classical Logic and Computation. PhD thesis, University of Cambridge, October
2000.
[WP08] Bruno Woltzenlogel Paleo. Herbrand Sequent Extraction. VDM-Verlag, Saarbruecken, Germany,
2008.
41