Search

By Gentzen's famous Hauptsatz the cut-elimination theorem every proof in sequent calculus for first-order logic with cuts can be transformed into a cut-free proof; cut-free proofs are analytic and consist entirely of syntactic material of the end-sequent the proven theorem. But in systems with induction rules, cut-elimination is either impossible or does not produce proofs with the subformula property. One way to overcome this problem is to formulate induction proofs as infinite sequences of proofs in a uniform way and to develop a method, which yields a uniform description of the corresponding cut-free proofs. We present such a formalism, as an alternative to systems with induction rules, and define a corresponding cut-elimination method based on the CERES-method for first-order logic. The basic tools of proof theory, such as sequent- and resolution calculi are enriched with inductive definitions and schemata of terms, formulas, proofs, etc. We define a class of inductive proofs which can be transformed into this formalism and subjected to schematic cut-elimination.

This paper introduces PROOFTOOL, the graphical user interface for the General Architecture for Proof Theory (GAPT) framework. Its features are described with a focus not only on the visualization but also on the analysis and transformation of proofs and related tree-like structures, and its implementation is explained. Finally, PROOFTOOL is compared with three other graphical interfaces for proofs., In Proceedings UITP 2012, arXiv:1307.1528