A simplified proof that regular resolution is exponential

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

Mordechai Ben-Ari

Publication date: 1980

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

Full work available at URL: https://doi.org/10.1016/s0020-0190(80)90082-4

zbMATH Keywords

proof treesregular resolution is exponential

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05) Complexity of proofs (03F20)

Related Items (1)

The complexity of Gentzen systems for propositional logic

Cites Work

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

This page was built for publication: A simplified proof that regular resolution is exponential