A simplified proof that regular resolution is exponential

DOI10.1016/S0020-0190(80)90082-4zbMath0438.03054MaRDI QIDQ1141648

Mordechai Ben-Ari

Publication date: 1980

Published in: Information Processing Letters (Search for Journal in Brave)

zbMATH Keywords

proof trees; regular resolution is exponential

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03D15: Complexity of computation (including implicit computational complexity)

03B05: Classical propositional logic

03F20: Complexity of proofs

Related Items

The complexity of Gentzen systems for propositional logic

Cites Work

• On the complexity of regular resolution and the Davis-Putnam procedure