{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:03Z","timestamp":1747592463363},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_28","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T06:13:46Z","timestamp":1437718426000},"page":"399-415","source":"Crossref","is-referenced-by-count":22,"title":["Playing with AVATAR"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning Chap. 2","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning Chap. 2, pp. 19\u201399. Elsevier Science, North-Holland (2001)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-38574-2_33","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Hoder","year":"2013","unstructured":"Hoder, K., Voronkov, A.: The 481 ways to split a clause and deal with propositional variables. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 450\u2013464. Springer, Heidelberg (2013)"},{"key":"28_CR4","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: Nebel, B. (ed.) 17th International Joint Conference on Artificial Intelligence, IJCAI 2001, vol. 1, pp. 611\u2013617 (2001)"},{"issue":"2\u20133","key":"28_CR5","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"1\u20132","key":"28_CR6","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symbolic Comput. 36(1\u20132), 101\u2013115 (2003)","journal-title":"J. Symbolic Comput."},{"issue":"4","key":"28_CR7","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. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1\u20132","key":"28_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001)","journal-title":"Artif. Intell."},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Heidelberg (2014)"},{"key":"28_CR10","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning Chap. 27","author":"C Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning Chap. 27, pp. 1965\u20132013. Elsevier Science, North-Holland (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T10:29:53Z","timestamp":1559212193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}