Sciweavers

Share
TLCA
2005
Springer

Semantic Cut Elimination in the Intuitionistic Sequent Calculus

8 years 12 months ago
Semantic Cut Elimination in the Intuitionistic Sequent Calculus
Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen’s intuitionistic sequent calculus LJ, that relies on completeness of the cutfree calculus with respect to Kripke Models. The proof defines a general framework to extend the cut elimination result to other intuitionistic deduction systems, in particular to deduction modulo provided the rewrite system verifies some properties. We also give an example of rewrite system for which cut elimination holds but that doesn’t enjoys proof normalization.
Olivier Hermant
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors Olivier Hermant
Comments (0)
books