Fast Cut-Elimination using Proof Terms: An Empirical Study

Fast Cut-Elimination using Proof Terms: An Empirical Study

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...

Full description

Bibliographic Details
Main Author: Gabriel Ebner
Format: Article
Language:English
Published: Open Publishing Association 2018-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1810.07373v1
id doaj-2e82ccee7ca14d8e9f77ec98f986cd83
record_format Article
spelling doaj-2e82ccee7ca14d8e9f77ec98f986cd832020-11-25T02:43:14ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-10-01281Proc. CL&C 2018243810.4204/EPTCS.281.3:2Fast Cut-Elimination using Proof Terms: An Empirical StudyGabriel Ebner0 TU Wien, Austria 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.http://arxiv.org/pdf/1810.07373v1
collection DOAJ
language English
format Article
sources DOAJ
author Gabriel Ebner
spellingShingle Gabriel Ebner
Fast Cut-Elimination using Proof Terms: An Empirical Study
Electronic Proceedings in Theoretical Computer Science
author_facet Gabriel Ebner
author_sort Gabriel Ebner
title Fast Cut-Elimination using Proof Terms: An Empirical Study
title_short Fast Cut-Elimination using Proof Terms: An Empirical Study
title_full Fast Cut-Elimination using Proof Terms: An Empirical Study
title_fullStr Fast Cut-Elimination using Proof Terms: An Empirical Study
title_full_unstemmed Fast Cut-Elimination using Proof Terms: An Empirical Study
title_sort fast cut-elimination using proof terms: an empirical study
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2018-10-01
description 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.
url http://arxiv.org/pdf/1810.07373v1
work_keys_str_mv AT gabrielebner fastcuteliminationusingprooftermsanempiricalstudy
_version_ 1724770589927800832

Similar Items