Depth of proofs, depth of cut-formulas and complexity of cut formulas

DOI10.1016/0304-3975(94)90087-6zbMath0807.03038OpenAlexW2022618710MaRDI QIDQ1329747

Wen-Hui Zhang

Publication date: 31 July 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90087-6

zbMATH Keywords

complexitycut-eliminationalternation of quantifiers

Mathematics Subject Classification ID

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

Related Items

Sharpened lower bounds for cut elimination, Structure of proofs and the complexity of cut elimination, On the elimination of quantifier-free cuts, Sufficient conditions for cut elimination with complexity analysis, Extracting Herbrand disjunctions by functional interpretation, On the form of witness terms, The role of quantifier alternations in cut elimination

Cites Work

• The number of proof lines and the size of proofs in first order logic
• Cut elimination and automatic proof procedures
• Unnamed Item