{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:43Z","timestamp":1725903403575},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_34","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"563-579","source":"Crossref","is-referenced-by-count":7,"title":["Monte Carlo Tableau Proof Search"],"prefix":"10.1007","author":[{"given":"Michael","family":"F\u00e4rber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"2","key":"34_CR1","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-28717-6_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Alama","year":"2012","unstructured":"Alama, J., K\u00fchlwein, D., Urban, J.: Automated and human proofs in general mathematics: an initial comparison. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 37\u201345. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_6"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_14"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-319-13647-9_39","volume-title":"Human-Inspired Computing and Its Applications","author":"A Biere","year":"2014","unstructured":"Biere, A., Dragan, I., Kov\u00e1cs, L., Voronkov, A.: Experimenting with SAT solvers in Vampire. In: Gelbukh, A., Espinoza, F.C., Galicia-Haro, S.N. (eds.) MICAI 2014. LNCS, vol. 8856, pp. 431\u2013442. Springer, Cham (2014). doi: 10.1007\/978-3-319-13647-9_39"},{"issue":"1","key":"34_CR5","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reasoning"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_11"},{"issue":"1","key":"34_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TCIAIG.2012.2186810","volume":"4","author":"C Browne","year":"2012","unstructured":"Browne, C., Powley, E.J., Whitehouse, D., Lucas, S.M., Cowling, P.I., Rohlfshagen, P., Tavener, S., Liebana, D.P., Samothrakis, S., Colton, S.: A survey of Monte Carlo tree search methods. IEEE Trans. Comput. Intell. AI Games 4(1), 1\u201343 (2012)","journal-title":"IEEE Trans. Comput. Intell. AI Games"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"F\u00e4rber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti and Tiwari [17], pp. 349\u2013361","DOI":"10.1007\/978-3-319-40229-1_24"},{"key":"34_CR9","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/1273496.1273531","volume-title":"ICML","author":"S Gelly","year":"2007","unstructured":"Gelly, S., Silver, D.: Combining online and offline knowledge in UCT. In: Ghahramani, Z. (ed.) ICML, vol. 227, pp. 273\u2013280. ACM, New York (2007)"},{"key":"34_CR10","first-page":"100","volume-title":"Handbook of Automated Reasoning","author":"R H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 100\u2013178. Elsevier and MIT Press, New York (2001)"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti and Tiwari [17], pp. 313\u2013329","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-319-21401-6_27","volume-title":"Automated Deduction \u2013 CADE-25","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Schulz, S., Urban, J., Vysko\u010dil, J.: System description: E.T. 0.1. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 389\u2013398. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_27"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-662-48899-7_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: FEMaLeCoP: fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 88\u201396. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_7"},{"key":"34_CR14","first-page":"59","volume-title":"CPP","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J., Vyskocil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Leroy, X., Tiu, A. (eds.) CPP, pp. 59\u201366. ACM, New York (2015)"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11871842_29","volume-title":"Machine Learning: ECML 2006","author":"L Kocsis","year":"2006","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based Monte-Carlo planning. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp. 282\u2013293. Springer, Heidelberg (2006). doi: 10.1007\/11871842_29"},{"key":"34_CR16","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 - Essays in Memory of Harald Ganzinger","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen \u2013 a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Ganzinger Festschrift. LNCS, vol. 7797, pp. 239\u2013270. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37651-1_10"},{"key":"34_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1","volume-title":"Automated Reasoning","year":"2016","unstructured":"Olivetti, N., Tiwari, A. (eds.): IJCAR 2016. LNCS (LNAI), vol. 9706. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1"},{"key":"34_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-71070-7_23","volume-title":"Automated Reasoning","author":"J Otten","year":"2008","unstructured":"Otten, J.: leanCoP 2.0 and ileanCoP 1.2: high performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 283\u2013291. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_23"},{"issue":"2\u20133","key":"34_CR19","doi-asserted-by":"crossref","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2\u20133), 159\u2013182 (2010)","journal-title":"AI Commun."},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Otten, J.: nanoCoP: a non-clausal connection prover. In: Olivetti and Tiwari [17], pp. 302\u2013312","DOI":"10.1007\/978-3-319-40229-1_21"},{"key":"34_CR21","first-page":"649","volume-title":"IJCAI","author":"CD Rosin","year":"2011","unstructured":"Rosin, C.D.: Nested rollout policy adaptation for Monte Carlo tree search. In: Walsh, T. (ed.) IJCAI, pp. 649\u2013654. IJCAI\/AAAI, New York (2011)"},{"key":"34_CR22","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.knosys.2011.08.008","volume":"34","author":"MPD Schadd","year":"2012","unstructured":"Schadd, M.P.D., Winands, M.H.M., Tak, M.J.W., Uiterwijk, J.W.H.M.: Single-player Monte-Carlo tree search for SameGame. Knowl.-Based Syst. 34, 3\u201311 (2012)","journal-title":"Knowl.-Based Syst."},{"issue":"2\u20133","key":"34_CR23","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"34_CR24","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 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_49"},{"key":"34_CR25","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D., Huang, A., Maddison, C.J., Guez, A., Sifre, L., van den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap, T., Leach, M., Kavukcuoglu, K., Graepel, T., Hassabis, D.: Mastering the game of Go with deep neural networks and tree search. Nature 529, 484\u2013503 (2016)","journal-title":"Nature"},{"issue":"2","key":"34_CR26","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/AIC-130550","volume":"26","author":"G Sutcliffe","year":"2013","unstructured":"Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition - CASC-J6. AI Commun. 26(2), 211\u2013223 (2013)","journal-title":"AI Commun."},{"key":"34_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15582-6_30","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"J Urban","year":"2010","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 155\u2013166. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15582-6_30"},{"key":"34_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-22119-4_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Urban","year":"2011","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: MaLeCoP machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 263\u2013277. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22119-4_21"},{"key":"34_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-20615-8_22","volume-title":"Intelligent Computer Mathematics","author":"M Wisniewski","year":"2015","unstructured":"Wisniewski, M., Steen, A., Benzm\u00fcller, C.: LeoPARD \u2014 a generic platform for the implementation of higher-order reasoners. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 325\u2013330. Springer, Cham (2015). doi: 10.1007\/978-3-319-20615-8_22"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T22:39:38Z","timestamp":1602455978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}