Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning

Samuel R. Buss, Jan Hoffmann, Jan Johannsen

Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there…