Structural cut elimination. I: Intuitionistic and classical logic

DOI10.1006/inco.1999.2832zbMath1005.03049OpenAlexW1546574044MaRDI QIDQ1854335

Frank Pfenning

Publication date: 14 January 2003

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

Full work available at URL: https://doi.org/10.1006/inco.1999.2832

zbMATH Keywords

cut elimination

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items

Towards Logical Frameworks in the Heterogeneous Tool Set Hets, A linear logic framework for multimodal logics, A dual-context sequent calculus for the constructive modal logic S4, Structural Focalization, A linear logical framework, Unnamed Item, Representing model theory in a type-theoretical logical framework, Focusing in Linear Meta-logic, A fresh view of linear logic as a logical framework, A logical framework combining model and proof theory, HADAMARD STATES FOR THE VECTOR POTENTIAL ON ASYMPTOTICALLY FLAT SPACETIMES, Representing Model Theory in a Type-Theoretical Logical Framework, Relating reasoning methodologies in linear logic and process algebra, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, Constructive linear-time temporal logic: proof systems and Kripke semantics, Unnamed Item, Mechanizing focused linear logic in Coq, Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Structural cut elimination. I: Intuitionistic and classical logic, A Linear Logic of Authorization and Knowledge, Redundancy Elimination for LF, A focused linear logical framework and its application to metatheory of object logics

Uses Software

• Coq
• Elf

Cites Work

• Linear logic
• On the unity of logic
• Computational interpretations of linear logic
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Untersuchungen über das logische Schliessen. I
• Structural cut elimination. I: Intuitionistic and classical logic
• Uniform proofs as a foundation for logic programming
• A framework for defining logics
• The correspondence between cut-elimination and normalization
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item