Cut elimination and automatic proof procedures

DOI10.1016/0304-3975(91)90086-HzbMath0745.68098WikidataQ127720171 ScholiaQ127720171MaRDI QIDQ1183598

Wen-Hui Zhang

Publication date: 28 June 1992

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

zbMATH Keywords

upper boundcut eliminationresolution

Mathematics Subject Classification ID

Related Items (11)

Depth of proofs, depth of cut-formulas and complexity of cut formulas ⋮ 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 ⋮ Cut formulas in propositional logic ⋮ Extracting Herbrand disjunctions by functional interpretation ⋮ On the form of witness terms ⋮ Corrected upper bounds for free-cut elimination ⋮ Weak logic theory ⋮ The role of quantifier alternations in cut elimination

Cites Work

• Don't eliminate cut
• Unnamed Item
• Unnamed Item

This page was built for publication: Cut elimination and automatic proof procedures