Reducing redundancy in cut-elimination by resolution

DOI10.1093/LOGCOM/EXU075zbMath1444.03163OpenAlexW2119935022MaRDI QIDQ2987066

Bruno Woltzenlogel Paleo

Publication date: 17 May 2017

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/062ec0c541b68df5dce624691ba7fb9b6fdc5686

zbMATH Keywords

cut eliminationsequent calculusproof theoryresolutionproof complexity

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items (3)

Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic ⋮ On the elimination of quantifier-free cuts ⋮ Physics and proof theory

Uses Software

• CERES
• ProofTool

This page was built for publication: Reducing redundancy in cut-elimination by resolution