@inproceedings{7573c8bd88994ba98601194942f5b5fe,
title = "Fast cut-elimination using proof terms: An empirical study",
abstract = "Urban and Bierman introduced a calculus of proof terms for the sequent calculus LK with a strongly normalizing reduction relation in [34]. 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.",
author = "Gabriel Ebner",
year = "2018",
month = oct,
day = "19",
doi = "10.4204/EPTCS.281.3",
language = "English",
volume = "281",
series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
publisher = "Open Publishing Association",
pages = "24--38",
booktitle = "7th International Workshop on Classical Logic and Computation, CL and C 2018; Oxford; United Kingdom; 7 July 2018 through",
note = "7th International Workshop on Classical Logic and Computation, CL and C 2018 ; Conference date: 07-07-2018",
}