Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments RTL(k) are related to clause learning algorithms where the width of learned clauses is bounded by k. For every k up to O(log n), an exponential separation between the proof systems RTL(k) and RTL(k + 1) is shown.
展开▼
