@misc{indiciae69bdeab17277,
  title = {Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning},
  author = {Samuel R. Buss and Jan Hoffmann and Jan Johannsen},
  year = {2008},
  doi = {10.2168/lmcs-4(4:13)2008},
  url = {https://arxiv.org/abs/0811.1075},
  note = {Source identifier: 0811.1075}
}