@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 22nd International Conference on Automated Deduction (CADE)", EDITOR = "Renate A. Schmidt", SERIES = "Lecture Notes in Artificial Intelligence", VOLUME = 5663, PAGES = "35--50", PUBLISHER = "Springer", MONTH = "August", DOI = "10.1007/978-3-642-02959-2_3", YEAR = 2009}