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

DOI10.1007/978-3-642-02261-6_17zbMath1246.03072OpenAlexW1510709103MaRDI QIDQ3638285

Hugo Herbelin, Gyesik Lee

Publication date: 2 July 2009

Published in: Logic, Language, Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02261-6_17

zbMATH Keywords

completenessKripke semanticscut-eliminationCoq proof assistantintuitionistic Gentzen-style sequent calculus

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Related Items (3)

Kripke models for classical logic ⋮ A henkin-style completeness proof for the modal logic S5 ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Constructivism in mathematics. An introduction. Volume II
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• A completeness theorem in modal logic
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• On weak completeness of intuitionistic predicate logic

This page was built for publication: Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus