Davis-Putnam resolution versus unrestricted resolution

DOI10.1007/BF01531027zbMath0865.03010MaRDI QIDQ1353991

Andreas Goerdt

Publication date: 13 May 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

Davis-Putnam resolutionproofs of superpolynomial lengthunrestricted resolution proofsunsatisfiable propositional formulas

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05)

Related Items (6)

Resolution and binary decision diagrams cannot simulate each other polynomially ⋮ The complexity of resolution refinements ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Expansion-based QBF solving versus Q-resolution ⋮ On Exponential Lower Bounds for Partially Ordered Resolution ⋮ Reflections on Proof Complexity and Counting Principles

Cites Work

• Unnamed Item
• Resolution proofs of generalized pigeonhole principles
• The intractability of resolution
• Unrestricted resolution versus N-resolution
• On the complexity of regular resolution and the Davis-Putnam procedure
• Many hard examples for resolution
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• A Computing Procedure for Quantification Theory

This page was built for publication: Davis-Putnam resolution versus unrestricted resolution