Fast cut-elimination using proof terms: an empirical study

## Author: Gabriel Ebner

## Paper Information

Title: | Fast cut-elimination using proof terms: an empirical study |

Authors: | Gabriel Ebner |

Proceedings: | CL&C Full papers and abstracts |

Editor: | Stefano Berardi |

Keywords: | cut-elimination, proof terms, Herbrand's theorem, expansion proofs |

Abstract: | 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 this calculus 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. |

Pages: | 15 |

Talk: | Jul 07 11:00 (Session 26A) |

Paper: |