Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic |
| |
Authors: | Dyckhoff Roy Pinto Luis |
| |
Affiliation: | (1) School of Mathematical & Computational Sciences, St Andrews University St Andrews, Scotland |
| |
Abstract: | We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz. |
| |
Keywords: | Cut-elimination normalisation natural deduction intuitionistic logic recursive path ordering termination |
本文献已被 SpringerLink 等数据库收录! |