Cut elimination inside a deep inference system for classical predicate logic

DOI10.1007/S11225-006-6605-4MaRDI QIDQ817702zbMATH OpenOpenAlexFDO

Authors Kai Brünnler

Publication date 17 March 2006

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://boris.unibe.ch/19297/1/11225_2006_Article_6605.pdf

zbMATH Keywords

cut eliminationdeep inferencefirst-order predicate logic

Mathematics Subject Classification ID

Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Deep inference and symmetry in classical proofs
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• From deep inference to proof nets via cut elimination
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• An Algorithmic Interpretation of a Deep Inference System

Cites work

• A system of interaction and structure
• Computer Science Logic
• Computer Science Logic
• Deep inference and symmetry in classical proofs
• Display logic
• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 1841813 (Why is no real title available?)
• On the limit products of a family of matrices

Cited in

(7)

• On the Power of Substitution in the Calculus of Structures
• A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
• Intermutation
• A Subatomic Proof System for Decision Trees
• Diagrammatic algebra of first order logic
• Non-elementary compression of first-order proofs in deep inference using epsilon-terms
• The calculus of neo-Peircean relations

This page was built for publication: Cut elimination inside a deep inference system for classical predicate logic

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