On the elimination of quantifier-free cuts

DOI10.1016/j.tcs.2011.08.035zbMath1241.03069OpenAlexW2053289767WikidataQ40389168 ScholiaQ40389168MaRDI QIDQ650922

Daniel Weller

Publication date: 7 December 2011

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.08.035

zbMATH Keywords

complexityfirst-order logiccut-eliminationHerbrand's theoremexponential upper boundquantifier-free cuts

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Describing proofs by short tautologies
• A compact representation of proofs
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Untersuchungen über das logische Schliessen. I
• The role of quantifier alternations in cut elimination
• Reducing redundancy in cut-elimination by resolution
• Lower bounds to the size of constant-depth propositional proofs
• The Complexity of Propositional Proofs
• Computer Science Logic
• Herbrand Sequent Extraction