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

DOI10.1007/978-3-642-02261-6_17MaRDI QIDQ3638285zbMATH OpenOpenAlexFDO

Authors 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

completenessCoq proof assistantcut-eliminationintuitionistic Gentzen-style sequent calculusKripke semantics

Mathematics Subject Classification ID

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

Recommendations

• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Cut elimination for Gentzen's sequent calculus with equality and logic of partial terms
• Typed Lambda Calculi and Applications
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Gentzen-style sequent calculus for semi-intuitionistic logic
• Cut elimination in nested sequents for intuitionistic modal logics
• scientific article; zbMATH DE number 1302675
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality

Cites work

• A completeness theorem in modal logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• Constructivism in mathematics. An introduction. Volume II
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 1555179 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Linear logic
• On weak completeness of intuitionistic predicate logic

Cited in

(7)

• A henkin-style completeness proof for the modal logic S5
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• Full cut elimination and interpolation for intuitionistic logic with existence predicate
• Typed Lambda Calculi and Applications
• Kripke models for classical logic
• Material dialogues for first-order logic in constructive type theory: extended version

Describes a project that uses

Uses Software

• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3638285)