{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:18:24Z","timestamp":1725520704471},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-89439-1_19","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"258-273","source":"Crossref","is-referenced-by-count":19,"title":["(LIA) - Model Evolution with Linear Integer Arithmetic Constraints"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Fuchs","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","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":"19_CR2","series-title":"LNAI","doi-asserted-by":"crossref","DOI":"10.1007\/b71631","volume-title":"Theory Reasoning in Connection Calculi","author":"P. Baumgartner","year":"1998","unstructured":"Baumgartner, P.: Theory Reasoning in Connection Calculi. LNCS (LNAI), vol.\u00a01527. Springer, Heidelberg (1998)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-73595-3_30","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. Baumgartner","year":"2007","unstructured":"Baumgartner, P.: Logical Engineering with Instance-Based Methods. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 404\u2013409. Springer, Heidelberg (2007)"},{"key":"19_CR4","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing Finite Models by Reduction to Function-Free Clause Logic. Journal of Applied Logic (in Press, 2007)"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the Model Evolution Calculus. International Journal of Artificial Intelligence Tools\u00a015(1), 21\u201352 (2006)","journal-title":"International Journal of Artificial Intelligence Tools"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: \u2013 Model Evolution With Linear Integer Arithmetic Constraints. Technical Report, Department of Computer Science, The University of Iowa (2008), http:\/\/www.cs.uiowa.edu\/~tinelli","DOI":"10.1007\/978-3-540-89439-1_19"},{"key":"19_CR7","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"19_CR8","series-title":"LNAI","first-page":"178","volume-title":"Proc. CADE-10","author":"H.J. B\u00fcrckert","year":"1990","unstructured":"B\u00fcrckert, H.J.: A Resolution Principle for Clauses with Constraints. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 178\u2013192. Springer, Heidelberg (1990)"},{"key":"19_CR9","series-title":"LNCS (LNAI)","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":"19_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y. Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603. Springer, Heidelberg (2007)"},{"key":"19_CR11","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)"},{"key":"19_CR12","unstructured":"Antonio, J., Per\u00e9z, N.: Encoding and Solving Problems in Effectively Propositional Logic. PhD thesis, The University of Manchester (2007)"},{"issue":"6","key":"19_CR13","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). J. of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. of the ACM"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier\/MIT press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"19_CR15","first-page":"333","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated Deduction by Theory Resolution. J. of Aut. R.\u00a01, 333\u2013355 (1985)","journal-title":"J. of Aut. R."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T13:12:41Z","timestamp":1557925961000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}