Invertibility in Sequent Calculi

MaRDI QIDQ7361215FDO

Authors Peter Chapman

Publication date 28 August 2009

Cites work

• A Declarative Language for the Coq Proof Assistant
• A new algorithm for derivability in the constructive propositional calculus
• A new constructive logic: classic logic
• A proof theory for generic judgments
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• Advanced Functional Programming
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Automated Deduction – CADE-20
• Barendregt’s Variable Convention in Rule Inductions
• Canonical Gentzen-Type Calculi with (n,k)-ary Quantifiers
• Computing interpolants in implicational logics
• Contraction-free sequent calculi for intuitionistic logic
• Display logic
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
• Extending intuitionistic linear logic with knotted structural rules
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Inductively defined types in the Calculus of Constructions
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Issues in the analysis of proof-search strategies in sequential presentations of logics
• Lectures on the Curry-Howard isomorphism
• Linear logic
• Logical Approaches to Computational Barriers
• Logical Approaches to Computational Barriers
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
• Modular Cut-Elimination: Finding Proofs or Counterexamples
• Nominal logic, a first order theory of names and binding
• Nominal reasoning techniques in Coq (extended abstract)
• On proof normalization in linear logic
• Permutability of proofs in intuitionistic sequent calculi
• Proof analysis in modal logic
• Proof theory
• Proving termination with multiset orderings
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• Simple consequence relations
• State of the Union: Type Inference Via Craig Interpolation
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• Strong normalisation of cut-elimination in classical logic
• Structural cut elimination. I: Intuitionistic and classical logic
• Structural proof theory. With an appendix by Aarne Ranta
• Structured Induction Proofs in Isabelle/Isar
• Sufficient conditions for cut elimination with complexity analysis
• Term Rewriting and All That
• The calculus of constructions
• The lambda calculus, its syntax and semantics
• The view from the left
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards a semantic characterization of cut-elimination

This page was built for software: Invertibility in Sequent Calculi