Sciweavers

WOLLIC
2009
Springer

Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus

13 years 10 months ago
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-free intuitionistic sequent calculus as formal system and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof, which has been formalised in the Coq proof assistant, easily extends to the case of the absurdity connective using Kripke models with exploding nodes.
Hugo Herbelin, Gyesik Lee
Added 25 May 2010
Updated 25 May 2010
Type Conference
Year 2009
Where WOLLIC
Authors Hugo Herbelin, Gyesik Lee
Comments (0)