Fast Cut-Elimination using Proof Terms: An Empirical Study

TL;DR

This paper presents an empirical study of a new, faster cut-elimination algorithm based on proof terms, extended to higher-order logic, and demonstrates significant performance improvements over existing methods.

Contribution

It introduces an extended calculus for higher-order logic with induction and equality, and implements a highly efficient cut-elimination algorithm in GAPT.

Findings

Algorithm is several orders of magnitude faster than Gentzen-like cut-reduction.

Performance is an order of magnitude better than existing GAPT procedures.

Effective on both artificial and real-world benchmarks.

Abstract

Urban and Bierman introduced a calculus of proof terms for the sequent calculus LK with a strongly normalizing reduction relation. We extend this calculus to simply-typed higher-order logic with inferences for induction and equality, albeit without strong normalization. We implement thiscalculus in GAPT, our library for proof transformations. Evaluating the normalization on both artificial and real-world benchmarks, we show that this algorithm is typically several orders of magnitude faster than the existing Gentzen-like cut-reduction, and an order of magnitude faster than any other cut-elimination procedure implemented in GAPT.