{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:31:08Z","timestamp":1725564668615},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152962"},{"type":"electronic","value":"9783642152979"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15297-9_8","type":"book-chapter","created":{"date-parts":[[2010,9,6]],"date-time":"2010-09-06T08:11:13Z","timestamp":1283760673000},"page":"77-91","source":"Crossref","is-referenced-by-count":19,"title":["Natural Domain SMT: A Preliminary Assessment"],"prefix":"10.1007","author":[{"given":"Scott","family":"Cotton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Bj\u00f8rner, N., Dutertre, B., de Moura, L.: Accelerating Lemma Learning Using Joins \u2013 DPLL(\u2294). In: Int. Conf. Logic for Programming, Artif. Intell. and Reasoning, LPAR (2008)"},{"key":"8_CR2","volume-title":"Handbook of Constraint Programming, ch. 16","author":"F. Benhamou","year":"2006","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch. 16. Elsevier, Amsterdam (2006)"},{"key":"8_CR3","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), http:\/\/www.SMT-LIB.org"},{"key":"8_CR4","first-page":"825","volume-title":"Frontiers in Artificial Intelligence and Applications, ch. 26","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories February 2009. Frontiers in Artificial Intelligence and Applications, ch. 26, vol.\u00a0185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-71070-7_40","volume-title":"Automated Reasoning","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Engineering DPLL(T) + Saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 475\u2013490. Springer, Heidelberg (2008)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Constraint Programming (2009)","DOI":"10.1007\/978-3-642-04244-7_41"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"CAV 2009","author":"K.L. McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to Richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 462\u2013476. Springer, Heidelberg (2009)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC\u201901 (2001)","DOI":"10.1145\/378239.379017"},{"key":"8_CR10","volume-title":"Handbook of Constraint Programming, ch. 12","author":"K. Marriott","year":"2006","unstructured":"Marriott, K., Stuckey, P.J., Wallace, M.: Constraint logic programming. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch. 12, Elsevier, Amsterdam (2006)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Wang, C., Gupta, A., Gannai, M.K.: Predicate Learning and Selective Theory Deduction. In: Design Automation Conference, DAC (2006)","DOI":"10.1145\/1146909.1146971"},{"key":"8_CR12","unstructured":"Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe Conference and Exhibition (DATE\u201903), p. 10880 (2003)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15297-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:04:32Z","timestamp":1606187072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15297-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152962","9783642152979"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15297-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}