{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:46:52Z","timestamp":1742932012106,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_9","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"85-100","source":"Crossref","is-referenced-by-count":10,"title":["Model Evolution with Equality Modulo Built-in Theories"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierachic first-order theories. Appl. Algebra Eng. Commun. Comput.\u00a05, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: ME(LIA) - model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 258\u2013273. Springer, Heidelberg (2008)"},{"key":"9_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/11532231_29","volume-title":"Automated Deduction \u2013 CADE-20","author":"P. Baumgartner","year":"2005","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus with Equality. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 392\u2013408. Springer, Heidelberg (2005)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-02959-2_2","volume-title":"Automated Deduction \u2013 CADE-22","author":"P. Baumgartner","year":"2009","unstructured":"Baumgartner, P., Waldmann, U.: Superposition and Model Evolution Combined. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 17\u201334. Springer, Heidelberg (2009)"},{"key":"9_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 497\u2013511. Springer, Heidelberg (2006)"},{"key":"9_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y. Ge","year":"2007","unstructured":"Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 167\u2013182. Springer, Heidelberg (2007)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"issue":"6","key":"9_CR9","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"9_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T03:13:06Z","timestamp":1553915586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}