Fast cut-elimination using proof terms: An empirical study

Gabriel Ebner*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publication7th International Workshop on Classical Logic and Computation, CL and C 2018; Oxford; United Kingdom; 7 July 2018 through
Pages24-38
Number of pages15
Volume281
DOIs
Publication statusPublished - 19 Oct 2018
Externally publishedYes
Event7th International Workshop on Classical Logic and Computation, CL and C 2018 - Oxford, United Kingdom
Duration: 7 Jul 2018 → …

Publication series

NameElectronic Proceedings in Theoretical Computer Science, EPTCS
PublisherOpen Publishing Association
ISSN (Print)2075-2180

Conference

Conference7th International Workshop on Classical Logic and Computation, CL and C 2018
Country/TerritoryUnited Kingdom
CityOxford
Period7/07/18 → …

Cite this