TY  - RPRT
TI  - Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
AU  - Samuel R. Buss
AU  - Jan Hoffmann
AU  - Jan Johannsen
PY  - 2008
DO  - 10.2168/lmcs-4(4:13)2008
UR  - https://arxiv.org/abs/0811.1075
ID  - 0811.1075
ER  -