Cut formulas in propositional logic

DOI10.1016/0304-3975(93)90249-SzbMath0788.03069OpenAlexW2083806359MaRDI QIDQ689298

Wen-Hui Zhang

Publication date: 20 December 1993

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

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90249-s

zbMATH Keywords

propositional logicresolution principlespeed upproof lengthanalysis treesatomic cutcut formulascut-free proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items

Relative efficiency of propositional proof systems: Resolution vs. cut-free LK

Cites Work

• Unnamed Item
• The intractability of resolution
• Cut elimination and automatic proof procedures
• The relative efficiency of propositional proof systems
• Bounds for proof-search and speed-up in the predicate calculus
• A Machine-Oriented Logic Based on the Resolution Principle