@INPROCEEDINGS{MPB-CL-LM:CADE2009:dpllSPutp,
AUTHOR = "Maria Paola Bonacina and Christopher A. Lynch and Leonardo de Moura",
TITLE = "On deciding satisfiability by {DPLL}({$\Gamma+\mathcal{T}$})
and unsound theorem proving",
BOOKTITLE = "Proceedings of the Twenty-second International Conference on
Automated Deduction (CADE)",
EDITOR = "Renate Schmidt",
PUBLISHER = "Springer",
SERIES = "Lecture Notes in Artificial Intelligence",
VOLUME = 5663,
PAGES = "35--50",
MONTH = "August",
YEAR = 2009}