{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:41:03Z","timestamp":1767339663526},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441908"},{"type":"electronic","value":"9783540457572"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45757-7_26","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T13:50:39Z","timestamp":1192888239000},"page":"308-319","source":"Crossref","is-referenced-by-count":23,"title":["A DPLL-Based Calculus for Ground Satisfiability Modulo Theories"],"prefix":"10.1007","author":[{"given":"Cesare","family":"Tinelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"26_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"SAT-based procedures for temporal reasoning","author":"A. Armando","year":"2000","unstructured":"Alessandro Armando, Claudio Castellini, and Enrico Giunchiglia. SAT-based procedures for temporal reasoning. In S. Biundo and M. Fox, editors, Proceedings of the 5th European Conference on Planning (Durham, UK), volume 1809of Lecture Notes in Computer Science, pages 97\u20131080. Springer, 2000."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani. A SAT-based approach for solving formulas over boolean and linear mathematical propositions. In Reiner H\u00e4hnle, editor, Proceedings of the 18th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence. Springer, 2002. (to appear).","DOI":"10.1007\/3-540-45620-1_17"},{"key":"26_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Validity checking for combinations of theories with equality","author":"C. W. Barrett","year":"1996","unstructured":"Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. Validity checking for combinations of theories with equality. In M. K. Srivas and A. Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (Palo Alto, CA), volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201. Springer, 1996."},{"key":"26_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Checking satisfiability of first-order formulas by incremental translation to SAT","author":"C. W. Barrett","year":"2002","unstructured":"Clark W. Barrett, David L. Dill, and Aaron Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In J. C. Godskesen, editor, Proceedings of the International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, 2002. (to appear)."},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Nikolaj S. Bj\u00f8rner, Mark. E. Stickel, and Tom\u00e1s E. Uribe. A practical integration of first-order reasoning and decision procedures. In W. McCune, editor, Proceedings of the 14th International Conference on Automated Deduction, CADE-14 (Townsville, Australia), volume 1249 of Lecture Notes in Artificial Intelligence, pages 101\u2013115, 1997.","DOI":"10.1007\/3-540-63104-6_13"},{"issue":"7","key":"26_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394\u2013397, July 1962.","journal-title":"Communications of the ACM"},{"issue":"3","key":"26_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201\u2013215, July 1960.","journal-title":"Journal of the ACM"},{"key":"26_CR8","unstructured":"Leonardo de Moura and Harald Rue\u00df. Lemmas on demand for satisfiability solvers. Presented at the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT\u201902), Cincinnati, USA, May 2002."},{"key":"26_CR9","unstructured":"Jon W. Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, Departement of computer and Information science, University of Pennsylvania, Philadelphia, 1995."},{"key":"26_CR10","unstructured":"Wilfrid Hodges. Logical features of Horn clauses. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, pages 449\u2013503. Oxford University Press, 1993."},{"key":"26_CR11","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"Joxan Jaffar and Michael Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19\/20:503\u2013581, 1994.","journal-title":"Journal of Logic Programming"},{"issue":"1","key":"26_CR12","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Shie-Jue Lee and David A. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1):25\u201342, August 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR13","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Cha.: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC\u201901), June 2001."},{"key":"26_CR14","unstructured":"Greg Nelson and Dave Detlefs. The Simplify user\u2019s manual. Compaq Systems Research Center. ( http:\/\/research.compaq.com\/SRC\/esc\/Simplify.html )."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Cesare Tinelli. A DPLL-based calculus for ground satisfiability modulo theories. Technical report, Department of Computer Science, University of Iowa, 2002.","DOI":"10.1007\/3-540-45757-7_26"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45757-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T18:07:43Z","timestamp":1556906863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45757-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441908","9783540457572"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45757-7_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}