{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:18:53Z","timestamp":1725830333722},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_6","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T00:20:53Z","timestamp":1442622053000},"page":"85-100","source":"Crossref","is-referenced-by-count":7,"title":["First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Teucke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"issue":"2&3","key":"6_CR1","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0304-3975(89)90006-6","volume":"67","author":"J.C.M. Baeten","year":"1989","unstructured":"Baeten, J.C.M., Bergstra, J.A., Klop, J.W., Weijland, W.P.: Term-rewriting systems with rule priorities. Theor. Comput. Sci.\u00a067(2&3), 283\u2013301 (1989)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR2","unstructured":"Giunchiglia, F., Giunchiglia, E.: Building complex derived inference rules: A decider for the class of prenex universal-existential formulas. In: ECAI, pp. 607\u2013609 (1988)"},{"issue":"2\u20133","key":"6_CR3","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","volume":"57","author":"F. Giunchiglia","year":"1992","unstructured":"Giunchiglia, F., Walsh, T.: A theory of abstraction. Artif. Intell.\u00a057(2\u20133), 323\u2013389 (1992)","journal-title":"Artif. Intell."},{"key":"6_CR4","unstructured":"Hobbs, J.R.: Granularity. In: Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pp. 432\u2013435. Morgan Kaufmann (1985)"},{"key":"6_CR5","first-page":"997","volume-title":"Proceedings of the 10th International Joint Conference on Artificial Intelligence","author":"T. Imielinski","year":"1987","unstructured":"Imielinski, T.: Domain abstraction and limited reasoning. In: Proceedings of the 10th International Joint Conference on Artificial Intelligence, vol.\u00a02, pp. 997\u20131003. Morgan Kaufmann Publishers Inc., San Francisco (1987)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K. Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen - A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol.\u00a07797, pp. 239\u2013270. Springer, Heidelberg (2013)"},{"issue":"3","key":"6_CR7","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reason.\u00a03(3), 301\u2013317 (1987)","journal-title":"J. Autom. Reason."},{"key":"6_CR8","volume-title":"Human Problem Solving","author":"A. Newell","year":"1972","unstructured":"Newell, A.: Human Problem Solving. Prentice-Hall, Inc., Upper Saddle River (1972)"},{"key":"6_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\u2013putnam\u2013logemann\u2013loveland procedure to dpll(t). Journal of the ACM\u00a053, 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D.A. Plaisted Theorem","year":"1981","unstructured":"Plaisted Theorem, D.A.: proving with abstraction. Artif. Intell.\u00a016(1), 47\u2013108 (1981)","journal-title":"Artif. Intell."},{"key":"6_CR11","first-page":"412","volume-title":"Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI 1973","author":"E.D. Sacerdott","year":"1973","unstructured":"Sacerdott, E.D.: Planning in a hierarchy of abstraction spaces. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI 1973, pp. 412\u2013422. Morgan Kaufmann Publishers Inc., San Francisco (1973)"},{"issue":"4","key":"6_CR12","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR13","unstructured":"Tenenberg, J.: Preserving consistency across abstraction mappings. In: Proceedings of the 10th IJCAI, International Joint Conference on Artificial Intelligence, pp. 1011\u20131014 (1987)"},{"key":"6_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, chapter 27, pp. 1965\u20132012. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T20:38:57Z","timestamp":1559248737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}