Algebraic proofs of cut elimination

DOI10.1016/S1567-8326(01)00009-1MaRDI QIDQ1349247zbMATH OpenOpenAlexWikidataFDO

Authors Jeremy Avigad

Publication date 21 May 2002

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1567-8326(01)00009-1, https://figshare.com/articles/journal_contribution/Algebraic_Proofs_of_Cut_Elimination/6490856

zbMATH Keywords

algebraic proofscut-elimination theorems

Mathematics Subject Classification ID

Recommendations

• Structural cut elimination. I: Intuitionistic and classical logic
• A note on the complexity of classical and intuitionistic proofs
• Minimal from classical proofs
• Publication:3475264
• A deconstruction of non-deterministic classical cut elimination

Cites work

• Constructive Sheaf Semantics
• Constructivism in mathematics. An introduction. Volume I
• Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik
• scientific article; zbMATH DE number 4134006 (Why is no real title available?)
• scientific article; zbMATH DE number 192927 (Why is no real title available?)
• scientific article; zbMATH DE number 1215498 (Why is no real title available?)
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• scientific article; zbMATH DE number 3348059 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Proof theory in the USSR 1925–1969
• Saturated models of universal theories
• Sheaves in geometry and logic: a first introduction to topos theory
• The correspondence between cut-elimination and normalization
• Transfer principles in nonstandard intuitionistic arithmetic
• Two applications of Boolean models

Cited in

(17)

• Algebraic aspects of cut elimination
• Saturated models of universal theories
• A deconstruction of non-deterministic classical cut elimination
• Unwinding a Non-effective Cut Elimination Proof
• scientific article; zbMATH DE number 4143971 (Why is no real title available?)
• scientific article; zbMATH DE number 408809 (Why is no real title available?)
• scientific article; zbMATH DE number 515726 (Why is no real title available?)
• scientific article; zbMATH DE number 742720 (Why is no real title available?)
• Algebraic cuts
• A note on the complexity of classical and intuitionistic proofs
• Forcing in Proof Theory
• Algebraic proof of the separation theorem on classical propositional calculus
• Types for Proofs and Programs
• An ecumenical notion of entailment
• No Speedup for Geometric Theories
• Kripke models for classical logic
• Double-negation elimination in some propositional logics

This page was built for publication: Algebraic proofs of cut elimination

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