Cut elimination inside a deep inference system for classical predicate logic

DOI10.1007/S11225-006-6605-4zbMATH Open1097.03047OpenAlexW2008876986MaRDI QIDQ817702FDOQ817702

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

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

zbMATH Keywords

cut eliminationfirst-order predicate logicdeep inference

Mathematics Subject Classification ID

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

Cites Work

• Display logic
• Title not available (Why is that?)
• Computer Science Logic
• A system of interaction and structure
• Title not available (Why is that?)
• On the limit products of a family of matrices
• Deep inference and symmetry in classical proofs
• Computer Science Logic

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)