{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T07:46:22Z","timestamp":1758267982172},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_22","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"313-329","source":"Crossref","is-referenced-by-count":21,"title":["Selecting the Selection"],"prefix":"10.1007","author":[{"given":"Kry\u0161tof","family":"Hoder","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Revised version in the J. Log. Comput. 4(3), 217\u2013247 (1994). Research Report MPI-I-91-208, Max-Planck-Institut f\u00fcr Informatik, 1991","key":"22_CR1","DOI":"10.1093\/logcom\/4.3.217"},{"doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, vol. I, chapter 2, pp. 19\u201399. Elsevier Science (2001)","key":"22_CR2","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a desision. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 83\u201396. Springer, Heidelberg (1993)"},{"doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Handbook of Automated Reasoning, vol. I, chapter 9, pp. 535\u2013610. Elsevier Science (2001)","key":"22_CR4","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"doi-asserted-by":"crossref","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2\u20135 July, pp. 295\u2013303. IEEE Computer Society (1999)","key":"22_CR5","DOI":"10.1109\/LICS.1999.782624"},{"doi-asserted-by":"crossref","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","key":"22_CR6","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, vol. I, chapter 7, pp. 371\u2013443. Elsevier Science (2001)","key":"22_CR8","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/978-3-319-21401-6_28","volume-title":"Automated Deduction - CADE-25","author":"G Reger","year":"2015","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Reger, G., Suda, M., Voronkov, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 399\u2013415. Springer, Switzerland (2015)"},{"unstructured":"Reger, G., Voronkov, A.: The Vampire manual. Technical report (2016, in preperation)","key":"22_CR10"},{"issue":"2\u20133","key":"22_CR11","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"unstructured":"Schulz, S.: E 1.8 User Manual (2015). http:\/\/wwwlehre.dhbw-stuttgart.de\/sschulz\/WORK\/E_DOWNLOAD\/V_1.9\/eprover.pdf . Accessed 22 Jan 2016","key":"22_CR12"},{"doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, I., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, vol. II, chapter 26, pp. 1853\u20131964. Elsevier Science (2001)","key":"22_CR13","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https:\/\/www.starexec.org","key":"22_CR14"},{"issue":"4","key":"22_CR15","doi-asserted-by":"crossref","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. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"22_CR16","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"key":"22_CR17","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)"},{"doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning, vol. II, chapter 27, pp. 1965\u20132013. Elsevier Science (2001)","key":"22_CR18","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T12:38:54Z","timestamp":1568032734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}