4 Clause Learning and Proper Natural Refinements of RES

We prove that the proof system CL, even without restarts, is stronger than all proper natural refinements of RES. We do this by first introducing a way of extending any CNF formula based on a given RES proof of it. We then show that if a formula F f (n)-separates RES from a natural refinement S, its extension f (n)-separates CL from S. The existence of such an F is guaranteed for all f (n)-proper natural refinements by definition.



Subsections
Journal of Artificial Intelligence Research 22 (2004). Copyright AI Access Foundation. All rights reserved.