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 eliminationfirst-order predicate logicdeep inference

Mathematics Subject Classification ID

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

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

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

Cited in

(4)

• Intermutation
• A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
• On the Power of Substitution in the Calculus of Structures
• A Subatomic Proof System for Decision Trees

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)