HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

Introduction

Proof analysis is a central mathematical activity which proved 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 (see e.g. Polya 1954a and Polya 1954b).

Cut-elimination, introduced by Gentzen, 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 analyzing mathematical proofs, especially to make implicit parameters explicit. In particular, cut free derivations admit the extraction of Herbrand disjunctions, which can be used for establishing bounds on existential quantifiers (e.g. see Luckhardt's analysis of the Theorem of Roth).

In a formal sense Girard's famous analysis of van der Waerden's theorem consists in the application of cut-elimination to the proof of Fürstenberg/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.

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 potentially produces new interesting proofs. Indeed, it is non-uniqueness which makes computational experiments with cut-elimination interesting (see Baaz, Hetzl, Leitsch, Richter and Spohr 2004). The experiments can be considered as a source for a base of proofs in formal format which provide different mathematical and computational information.

CERES (see Baaz and Leitsch 2000 and Baaz and Leitsch 2006) 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 CERES this method of cut-elimination 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 from LK to LKDe, a calculus containing definition introductions and equality rules (see Leitsch and Richter 2005 and Baaz, Hetzl, Leitsch, Richter and Spohr 2006), moves the system closer to real mathematical proofs.

Another step is the extension of CERES to second and higher order logic (see Hetzl, Leitsch, Weller and Woltzenlogel Paleo 2009, Weller 2010 and Hetzl, Leitsch and Weller 2011). Since proof Skolemization does not carry over to higher order logic, eigenvariables are replaced by Skolem terms in the sequent calculus LKsk. Now the proof projections may become locally unsound due to eigenvariable violations, still they fulfill some global soundness conditions which allows to transform them back to LK. The system CERES was extended within the Generic architecture for proofs framework in order to support these features.

An alternative approach to higher order logic is the extension of CERES to a schematic sequent calculus LKsch defined by primitve recursion. In the first step, a restricted class of cuts over propositional proofs is analyzed. The next goal is the generalization to first order formulas. Research in this direction is undertaken in a joint project with the CAPP at the Laboratoire d'Informatique de Grenoble.