{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:17:01Z","timestamp":1725560221717},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_29","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"392-408","source":"Crossref","is-referenced-by-count":17,"title":["The Model Evolution Calculus with Equality"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","first-page":"353","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, Foundations. Calculi and Refinements, vol.\u00a0I, pp. 353\u2013398. Kluwer, Dordrecht (1998)"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/10721959_16","volume-title":"Automated Deduction - CADE-17","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL \u2013 A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 200\u2013219. Springer, Heidelberg (2000)"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the Model Evolution Calculus. In: International Journal on Artificial Intelligence Tools, IJAIT (2005) (to appear)","DOI":"10.1142\/S0218213006002552"},{"key":"29_CR4","series-title":"Lecture Notes in Artificial Intelligence","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":"29_CR5","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus with Equality (2005), http:\/\/www.mpi-sb.mpg.de\/~baumgart\/publications\/MEE.pdf","DOI":"10.1007\/11532231_29"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","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, vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"issue":"7","key":"29_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"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-30124-0_9","volume-title":"Computer Science Logic","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 71\u201384. Springer, Heidelberg (2004)"},{"key":"29_CR9","unstructured":"Ganzinger, H., Korovin, K.: New Directions in Instance-Based Theorem Proving. In: Proc. LICS (2003)"},{"key":"29_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45616-3_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 176\u2013190. Springer, Heidelberg (2002)"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"29_CR12","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"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:47:05Z","timestamp":1635727625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11532231_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}