{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:46Z","timestamp":1751660506134,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_32","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"350-364","source":"Crossref","is-referenced-by-count":45,"title":["The Model Evolution Calculus"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","volume-title":"Automated Deduction. A Basis for Applications","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Equational Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications, vol.\u00a0I, ch. 11, Kluwer, Dordrecht (1998)"},{"key":"32_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-69778-0_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"P. Baumgartner","year":"1998","unstructured":"Baumgartner, P.: Hyper Tableaux\u2014The Next Generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 60\u201376. Springer, Heidelberg (1998)"},{"key":"32_CR3","series-title":"LNAI","volume-title":"Automated Deduction - CADE-17","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL\u2014A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831. Springer, Heidelberg (2000)"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. Fachberichte Informatik 1\u20132003, Universit\u00e4t Koblenz-Landau (2003)","DOI":"10.1007\/978-3-540-45085-6_32"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg (1982)","DOI":"10.1007\/978-3-322-90100-2"},{"key":"32_CR6","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The Disconnection Method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"issue":"7","key":"32_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"32_CR8","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"32_CR9","unstructured":"Ganzinger, H., Korovin, K.: New directions in instance-based theorem proving. In: LICS - Logics in Computer Science (2003) (to appear)"},{"key":"32_CR10","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J.N. Hooker","year":"2002","unstructured":"Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial Instantiation Methods for Inference in First Order Logic. Journal of Automated Reasoning\u00a028, 371\u2013396 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR11","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J., Plaisted, D.: Eliminating Duplicates with the Hyper-Linking Strategy. Journal of Automated Reasoning\u00a09, 25\u201342 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning\u00a013 (1994)","DOI":"10.1007\/BF00881947"},{"key":"32_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and Model Generation with Disconnection Tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, p. 142. Springer, Heidelberg (2001)"},{"issue":"3","key":"32_CR14","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. Journal of Automated Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-45616-3_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"G. Stenz","year":"2002","unstructured":"Stenz, G.: DCTP 1.2 - System Abstract. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 335\u2013340. Springer, Heidelberg (2002)"},{"key":"32_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-45757-7_26","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2002","unstructured":"Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol.\u00a02424, p. 308. Springer, Heidelberg (2002)"},{"issue":"1","key":"32_CR17","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1023\/A:1020512924736","volume":"29","author":"A. Yahya","year":"2002","unstructured":"Yahya, A., Plaisted, D.A.: Ordered Semantic Hyper-Tableaux. Journal of Automated Reasoning\u00a029(1), 17\u201357 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR18","unstructured":"Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. In: Proc. of AIMATH 1996 (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T07:31:23Z","timestamp":1740641483000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}