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...
| Päätekijä: | |
|---|---|
| Aineistotyyppi: | Artikkeli |
| Kieli: | English |
| Julkaistu: |
Open Publishing Association
2018-10-01
|
| Sarja: | Electronic Proceedings in Theoretical Computer Science |
| Linkit: | http://arxiv.org/pdf/1810.07373v1 |