{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T08:11:19Z","timestamp":1758269479044,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_23","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"339-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Cooperating Proof Attempts"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[]},{"given":"Dmitry","family":"Tishkovsky","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, Chap. 2, pp. 19\u201399. Elsevier Science, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"issue":"1\u20134","key":"23_CR3","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1023\/A:1018932114059","volume":"29","author":"M Bonacina","year":"2000","unstructured":"Bonacina, M.: A taxonomy of parallel strategies for deduction. Ann. Math. Artif. Intell. 29(1\u20134), 223\u2013257 (2000)","journal-title":"Ann. Math. Artif. Intell."},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"KI-96: Advances in Artificial Intelligence","author":"J Denzinger","year":"1996","unstructured":"Denzinger, J., Kronenburg., M.: Planning for distributed theorem proving: the teamwork approach. In: G\u00f6rz, G., H\u00f6lldobler, S. (eds.) KI 1996. LNCS, vol. 1137. Springer, Heidelberg (1996)"},{"issue":"2","key":"23_CR5","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT \u2013 a distributed and learning equational prover. J. Autom. Reasoning 18(2), 189\u2013198 (1997)","journal-title":"J. Autom. Reasoning"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of LICS 2003, pp. 55\u201364 (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"23_CR7","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":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-38574-2_28","volume-title":"Automated Deduction \u2013 CADE-24","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Schulz, S., Urban, J.: E-MaLeS 1.1. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 407\u2013413. Springer, Heidelberg (2013)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55425-4_6","volume-title":"Parallelization in Inference Systems","author":"E Lusk","year":"1992","unstructured":"Lusk, E., McCune, W.: Experiments with ROO: a parallel automated deduction system. In: Fronh\u00f6fer, B., Wrightson, G. (eds.) Dagstuhl Seminar 1990. LNCS, vol. 590. Springer, Heidelberg (1992)"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Proceedings of CADE2015 (2015)","DOI":"10.1007\/978-3-319-21401-6_28"},{"issue":"1\u20132","key":"23_CR12","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. Symb. Comp. 36(1\u20132), 101\u2013115 (2003)","journal-title":"J. Symb. Comp."},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-52885-7_78","volume-title":"10th International Conference on Automated Deduction","author":"J Schumann","year":"1990","unstructured":"Schumann, J., Letz, R.: PARTHEO: a high-performance parallel theorem prover. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 40\u201356. Springer, Heidelberg (1990)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/3-540-52885-7_77","volume-title":"10th International Conference on Automated Deduction","author":"JK Slaney","year":"1990","unstructured":"Slaney, J.K., Lusk, E.L.: Parallelizing the closure computation in automated deduction. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 28\u201339. Springer, Heidelberg (1990)"},{"key":"23_CR16","unstructured":"StarExec, https:\/\/www.starexec.org"},{"key":"23_CR17","unstructured":"Sutcliffe, G.: The design and implementation of a compositional competition-cooperation parallel ATP system. In: Proceedings IWIL-2, number MPI-I-2001-2-006 in MPI f\u00fcr Informatik, Research Report, pp. 92\u2013102 (2001)"},{"issue":"4","key":"23_CR18","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":"23_CR19","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":"23_CR20","doi-asserted-by":"crossref","unstructured":"Suttner, C.B., Schumann, J.: Chapter 9 \u2013 Parallel automated theorem proving. In: Parallel Processing for Artificial Intelligence, vol. 14 of Machine Intelligence and Pattern Recognition, pp. 209\u2013257. North-Holland (1994)","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"issue":"2","key":"23_CR21","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. J. Autom. Reasoning 18(2), 199\u2013204 (1997)","journal-title":"J. Autom. Reasoning"},{"key":"23_CR22","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":"23_CR23","unstructured":"Wolf, A., Fuchs, M.: Cooperative parallel automated theorem proving. Technical report SFB Bereicht 342\/21\/97, Technische Universit\u00e4t M\u00fcnchen (1997)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T17:11:22Z","timestamp":1748538682000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}