{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:47:43Z","timestamp":1725472063010},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482819"},{"type":"electronic","value":"9783540482826"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916277_39","type":"book-chapter","created":{"date-parts":[[2006,10,17]],"date-time":"2006-10-17T14:32:59Z","timestamp":1161095579000},"page":"572-586","source":"Crossref","is-referenced-by-count":18,"title":["Lemma Learning in the Model Evolution Calculus"],"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":"39_CR1","series-title":"LNCS (LNAI)","volume-title":"Automated Deduction - CADE-11","author":"O.L. Astrachan","year":"1992","unstructured":"Astrachan, O.L., Stickel, M.E.: Caching and Lemmaizing in Model Elimination Theorem Provers. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607. Springer, Heidelberg (1992)"},{"issue":"1","key":"39_CR2","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":"39_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma Learning in the Model Evolution Calculus. Technical Report no.\u00a006-04, Department of Computer Science, The University of Iowa (2006), Available at: http:\/\/www.cs.uiowa.edu\/~tinelli\/papers.html","DOI":"10.1007\/11916277_39"},{"key":"39_CR4","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C., de Nivelle, H., Tinelli, C.: Computing Finite Models by Reduction to Function-Free Clause Logic. In: Ahrendt, W., Baumgartner, P., de Nivelle, H. (eds.) IJCAR 2006 Workshop on Disproving (2006)"},{"key":"39_CR5","series-title":"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":"39_CR6","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"Peter Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. Fachberichte Informatik 1\u20132003, Universit\u00e4t Koblenz-Landau, Germany (2003)"},{"key":"39_CR7","unstructured":"Claessen, K., S\u00f6rensson, N.: New Techniques that Improve MACE-Style Finite Model Building. In: Baumgartner, P., Ferm\u00fcller, C.G. (eds.) CADE-19 Workshop on Model Computation (2003)"},{"key":"39_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Automated Reasoning","author":"H. Nivelle de","year":"2006","unstructured":"de Nivelle, H., Meng, J.: Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 303\u2013317. Springer, Heidelberg (2006)"},{"issue":"2","key":"39_CR9","first-page":"145","volume":"1","author":"G. DeJong","year":"1986","unstructured":"DeJong, G., Mooney, R.J.: Explanation-Based Learning: An Alternative View. Machine Learning\u00a01(2), 145\u2013176 (1986)","journal-title":"Machine Learning"},{"key":"39_CR10","unstructured":"Fuchs, A.: Darwin: A Theorem Prover for the Model Evolution Calculus. Master\u2019s thesis, University of Koblenz-Landau (2004)"},{"key":"39_CR11","volume-title":"Handbook of Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model Elimination and Connection Tableau Procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, Elsevier, Amsterdam (2001)"},{"key":"39_CR12","volume-title":"Automated Theorem Proving - A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"Loveland, D.: Automated Theorem Proving - A Logical Basis. North Holland, Amsterdam (1978)"},{"key":"39_CR13","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 Reference Manual and Guide. Technical Report ANL\/MCS-TM-264, Argonne National Laboratory (2003)","DOI":"10.2172\/822574"},{"key":"39_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-32275-7_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and Abstract DPLL Modulo Theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"39_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(94)90077-9","volume":"69","author":"A. Segre","year":"1994","unstructured":"Segre, A., Elkan, C.: A High-Performance Explanation-Based Learning Algorithm. Artificial Intelligence\u00a069, 1\u201350 (1994)","journal-title":"Artificial Intelligence"}],"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\/11916277_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:58:21Z","timestamp":1605625101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916277_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482819","9783540482826"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11916277_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}