{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T07:09:12Z","timestamp":1774940952218,"version":"3.50.1"},"reference-count":87,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,9,5]],"date-time":"2020-09-05T00:00:00Z","timestamp":1599264000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,9,5]],"date-time":"2020-09-05T00:00:00Z","timestamp":1599264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"European Research Council","award":["649043"],"award-info":[{"award-number":["649043"]}]},{"name":"European Research Council","award":["714034"],"award-info":[{"award-number":["714034"]}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"crossref","award":["CZ.02.1.01\/0.0\/0.0\/15_003\/0000466"],"award-info":[{"award-number":["CZ.02.1.01\/0.0\/0.0\/15_003\/0000466"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: first, we show optimised functional implementations of connection tableaux proof search, including a consistent Skolemisation procedure for machine learning. Then, we show two guidance methods based on machine learning, namely reordering of proof steps with Naive Bayesian probabilities, and expansion of a proof search tree with Monte Carlo Tree Search.\n<\/jats:p>","DOI":"10.1007\/s10817-020-09576-7","type":"journal-article","created":{"date-parts":[[2020,9,5]],"date-time":"2020-09-05T06:02:52Z","timestamp":1599285772000},"page":"287-320","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Machine Learning Guidance for Connection Tableaux"],"prefix":"10.1007","volume":"65","author":[{"given":"Michael","family":"F\u00e4rber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"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":[[2020,9,5]]},"reference":[{"key":"9576_CR1","doi-asserted-by":"publisher","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-18, vol. 7180 of LNCS, 37\u201345. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_6. ISBN 978-3-642-28716-9","DOI":"10.1007\/978-3-642-28717-6_6"},{"issue":"2","key":"9576_CR2","doi-asserted-by":"publisher","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. Reason. 52(2), 191\u2013213 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9286-5","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9576_CR3","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"PB Andrews","year":"1989","unstructured":"Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257\u2013291 (1989). https:\/\/doi.org\/10.1007\/BF00248320","journal-title":"J. Autom. Reason."},{"key":"9576_CR4","doi-asserted-by":"publisher","unstructured":"Armando, A., Baumgartner, P., Dowek, G. (eds.): IJCAR, vol. 5195 of LNCS. Springer (2008).https:\/\/doi.org\/10.1007\/978-3-540-71070-7. ISBN 978-3-540-71069-1","DOI":"10.1007\/978-3-540-71070-7"},{"issue":"3","key":"9576_CR5","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B Beckert","year":"1995","unstructured":"Beckert, B., Posegga, J.: leanTAP: lean tableau-based deduction. J. Autom. Reason. 15(3), 339\u2013358 (1995). https:\/\/doi.org\/10.1007\/BF00881804","journal-title":"J. Autom. Reason."},{"key":"9576_CR6","doi-asserted-by":"publisher","unstructured":"Beckert, Bernhard, H\u00e4hnle, Reiner, Schmitt, Peter H.: The even more liberalized $$\\delta $$-rule in free variable semantic tableaux. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Kurt g\u00f6del colloquium, vol. 713 of LNCS, pp. 108\u2013119. Springer (1993). https:\/\/doi.org\/10.1007\/BFb0022559. ISBN 3-540-57184-1","DOI":"10.1007\/BFb0022559"},{"key":"9576_CR7","doi-asserted-by":"publisher","unstructured":"Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.): TPHOLs, vol. 5674 of LNCS. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9. ISBN 978-3-642-03358-2","DOI":"10.1007\/978-3-642-03359-9"},{"key":"9576_CR8","doi-asserted-by":"publisher","unstructured":"Bertot, Y.: A short presentation of Coq. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, vol. 5170 of LNCS, pp. 12\u201316. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_3. ISBN 978-3-540-71065-3","DOI":"10.1007\/978-3-540-71067-7_3"},{"issue":"11","key":"9576_CR9","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W Bibel","year":"1983","unstructured":"Bibel, W.: Matings in matrices. Commun. ACM 26(11), 844\u2013852 (1983). https:\/\/doi.org\/10.1145\/182.183","journal-title":"Commun. ACM"},{"key":"9576_CR10","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Artificial Intelligence. Vieweg (1987). http:\/\/www.worldcat.org\/oclc\/16641802","DOI":"10.1007\/978-3-322-90102-6"},{"key":"9576_CR11","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Perspectives on automated deduction. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe. Automated Reasoning Series, pp. 77\u2013104. Kluwer Academic Publishers (1991). ISBN 0-7923-1409-3","DOI":"10.1007\/978-94-011-3488-0_4"},{"key":"9576_CR12","doi-asserted-by":"publisher","unstructured":"Bibel, W.: A vision for automated deduction rooted in the connection method. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX, vol. 10501 of LNCS, pp. 3\u201321. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_1. ISBN 978-3-319-66901-4","DOI":"10.1007\/978-3-319-66902-1_1"},{"key":"9576_CR13","doi-asserted-by":"publisher","unstructured":"Biere, A., Dragan, I., Kov\u00e1cs, L., Voronkov, A.: Experimenting with SAT solvers in Vampire. In: Gelbukh, A.F., Castro, F., Espinoza, Q., Galicia, S.N., Haro, Q. (eds.) MICAI 2014. part I, vol. 8856 of LNCS, pp. 431\u2013442. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-13647-9_39. ISBN 978-3-319-13646-2","DOI":"10.1007\/978-3-319-13647-9_39"},{"issue":"1","key":"9576_CR14","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formaliz. Reason."},{"issue":"3","key":"9576_CR15","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Greenaway, D., Kaliszyk, C., K\u00fchlwein, D., Urban, J.: A learning-based fact selector for Isabelle\/HOL. J. Autom. Reason. 57(3), 219\u2013244 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9362-8","journal-title":"J. Autom. Reason."},{"key":"9576_CR16","doi-asserted-by":"publisher","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda\u2014a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs, vol. 5674 of LNCS, pp. 73\u201378. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6. ISBN 978-3-642-03358-2","DOI":"10.1007\/978-3-642-03359-9_6"},{"issue":"1","key":"9576_CR17","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/TCIAIG.2012.2186810","journal-title":"IEEE Trans. Comput. Intell. AI Games"},{"key":"9576_CR18","doi-asserted-by":"publisher","unstructured":"Br\u00fcnnler, K., Metcalfe, G. (eds.). TABLEAUX, vol. 6793 of LNCS. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4. ISBN 978-3-642-22118-7","DOI":"10.1007\/978-3-642-22119-4"},{"key":"9576_CR19","unstructured":"Carlson, A.J., Cumby, C.M., Rosen, J.L., Roth, D.: SNoW user guide, Technical Report UIUCDCS-R-99-2101, University of Illinois at Urbana-Champaign (1999). http:\/\/cogcomp.org\/papers\/CCRR99.pdf"},{"key":"9576_CR20","unstructured":"Denzinger, J., Fuchs, M., Goller, C., Schulz, S.: Learning from Previous Proof Experience, Technical Report AR99-4, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"key":"9576_CR21","doi-asserted-by":"publisher","unstructured":"F\u00e4rber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) IJCAR, vol. 9706 of LNCS, pp. 349\u2013361. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_24. ISBN 978-3-319-40228-4","DOI":"10.1007\/978-3-319-40229-1_24"},{"key":"9576_CR22","doi-asserted-by":"publisher","unstructured":"F\u00e4rber, M., Kaliszyk, C., Urban, J.: Monte Carlo tableau proof search. In: de Moura, L. (ed.) CADE-26, vol. 10395 of LNCS, pp. 563\u2013579. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_34. ISBN 978-3-319-63045-8","DOI":"10.1007\/978-3-319-63046-5_34"},{"issue":"1\u20132","key":"9576_CR23","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0304-3975(99)00176-0","volume":"232","author":"D Galmiche","year":"2000","unstructured":"Galmiche, D.: Connection methods in linear logic and proof nets construction. Theor. Comput. Sci. 232(1\u20132), 231\u2013272 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00176-0","journal-title":"Theor. Comput. Sci."},{"key":"9576_CR24","doi-asserted-by":"publisher","unstructured":"Giese, M., Ahrendt, W.: Hilbert\u2019s epsilon-terms in automated theorem proving. In: Murray, N.V. (ed.)TABLEAUX, vol. 1617 of LNCS, pp. 171\u2013185. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48754-9_17. ISBN 3-540-66086-0","DOI":"10.1007\/3-540-48754-9_17"},{"key":"9576_CR25","unstructured":"Greenbaum, S.: Input transformations and resolution implementation techniques for theorem-proving in first-order logic. Ph.D. diss, University of Illinois at Urbana-Champaign (1986)"},{"key":"9576_CR26","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 100\u2013178. Elsevier, MIT Press (2001). ISBN 0-444-50813-9","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"9576_CR27","doi-asserted-by":"publisher","unstructured":"Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5. (2017). https:\/\/doi.org\/10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"key":"9576_CR28","doi-asserted-by":"publisher","unstructured":"Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs, vol. 5674 of LNCS, pp. 60\u201366. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4. ISBN 978-3-642-03358-2","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"9576_CR29","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik. II, vol. 50 of Die Grundlehren der mathematischen Wissenschaften. Springer (1939)"},{"issue":"2","key":"9576_CR30","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1305\/ndjfl\/1093883627","volume":"23","author":"J Hintikka","year":"1982","unstructured":"Hintikka, J.: Game-theoretical semantics: insights and prospects. Notre Dame J. Form. Log. 23(2), 219\u2013241 (1982). https:\/\/doi.org\/10.1305\/ndjfl\/1093883627","journal-title":"Notre Dame J. Form. Log."},{"key":"9576_CR31","doi-asserted-by":"publisher","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Stokkermans, V.S. (eds.) CADE-23, vol. 6803 of LNCS, pp. 299\u2013314. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_23. ISBN 978-3-642-22437-9","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"9576_CR32","doi-asserted-by":"publisher","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR, vol. 9706 of LNCS, pp. 313\u2013329. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_22. ISBN 978-3-319-40228-4","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"9576_CR33","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and application of strategies\/tactics in higher order logics (STRATA). NASA technical reports, pp. 56\u201368 (2003). http:\/\/www.gilith.com\/research\/papers"},{"key":"9576_CR34","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., E\u00e9n, N., Chollet, F., Urban, J.: DeepMath\u2014deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) NIPS, pp. 2235\u20132243 (2016). http:\/\/papers.nips.cc\/paper\/6280-deepmath-deep-sequence-models-for-premise-selection"},{"key":"9576_CR35","doi-asserted-by":"publisher","unstructured":"Jakub$$\\mathring{{\\rm u}}$$v, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM, vol. 10383 of LNCS, pp. 292\u2013302. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20. ISBN 978-3-319-62074-9","DOI":"10.1007\/978-3-319-62075-6_20"},{"issue":"11","key":"9576_CR36","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1016\/0020-0271(73)90043-0","volume":"9","author":"KS Jones","year":"1973","unstructured":"Jones, K.S.: Index term weighting. Inf. Storage Retr. 9(11), 619\u2013633 (1973). https:\/\/doi.org\/10.1016\/0020-0271(73)90043-0","journal-title":"Inf. Storage Retr."},{"issue":"2","key":"9576_CR37","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9303-3","journal-title":"J. Autom. Reason."},{"key":"9576_CR38","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, vol. 9450 of LNCS, pp. 88\u201396. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_7. ISBN 978-3-662-48898-0","DOI":"10.1007\/978-3-662-48899-7_7"},{"issue":"1","key":"9576_CR39","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015). https:\/\/doi.org\/10.1007\/s11786-014-0182-0","journal-title":"Math. Comput. Sci."},{"issue":"3","key":"9576_CR40","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9330-8","journal-title":"J. Autom. Reason."},{"key":"9576_CR41","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Leroy, X., Tiu, A. (eds.) CPP, pp. 59\u201366. ACM (2015). https:\/\/doi.org\/10.1145\/2676724.2693176. ISBN 978-1-4503-3296-5","DOI":"10.1145\/2676724.2693176"},{"key":"9576_CR42","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) IJCAI, pp. 3084\u20133090. AAAI Press (2015). ISBN 978-1-57735-738-4. http:\/\/ijcai.org\/Abstract\/15\/435"},{"key":"9576_CR43","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Schulz, S., Urban, J., Vysko\u010dil, J.: System description: E.T. 0.1. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25, vol. 9195 of LNCS, pp. 389\u2013398. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_27. ISBN 978-3-319-21400-9","DOI":"10.1007\/978-3-319-21401-6_27"},{"key":"9576_CR44","doi-asserted-by":"publisher","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based Monte-Carlo planning. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML, vol. 4212 of LNCS, pp. 282\u2013293. Springer (2006). https:\/\/doi.org\/10.1007\/11871842_29. ISBN 3-540-45375-X","DOI":"10.1007\/11871842_29"},{"key":"9576_CR45","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV, vol. 8044 of LNCS, pp. 1\u201335. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1. ISBN 978-3-642-39798-1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9576_CR46","doi-asserted-by":"publisher","unstructured":"K\u00fchlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR, vol. 7364 of LNCS, pp. 378\u2013392. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_30. ISBN 978-3-642-31364-6","DOI":"10.1007\/978-3-642-31365-3_30"},{"key":"9576_CR47","doi-asserted-by":"publisher","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP, vol. 7998 of LNCS, pp. 35\u201350. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6","DOI":"10.1007\/978-3-642-39634-2_6"},{"key":"9576_CR48","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 2015\u20132114. Elsevier, MIT Press (2001). ISBN 0-444-50813-9","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"issue":"2","key":"9576_CR49","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reason. 8(2), 183\u2013212 (1992). https:\/\/doi.org\/10.1007\/BF00244282","journal-title":"J. Autom. Reason."},{"key":"9576_CR50","unstructured":"Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21, vol. 46 of Epic series in computing, pp. 85\u2013105. EasyChair (2017). http:\/\/www.easychair.org\/publications\/paper\/340345"},{"issue":"2","key":"9576_CR51","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"DW Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem-proving by model elimination. J. ACM 15(2), 236\u2013251 (1968). https:\/\/doi.org\/10.1145\/321450.321456","journal-title":"J. ACM"},{"issue":"1","key":"9576_CR52","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41\u201357 (2009). https:\/\/doi.org\/10.1016\/j.jal.2007.07.004","journal-title":"J. Appl. Log."},{"key":"9576_CR53","doi-asserted-by":"publisher","unstructured":"Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.). TPHOLs, vol. 5170 of LNCS. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7. ISBN 978-3-540-71065-3","DOI":"10.1007\/978-3-540-71067-7"},{"key":"9576_CR54","unstructured":"Nonnengart, A.: Strong skolemization, Research Report MPI-I-96-2-010, Max-Planck-Institut f\u00fcr Informatik, Im Stadtwald, Saarbr\u00fccken, Germany (1996)"},{"key":"9576_CR55","doi-asserted-by":"publisher","unstructured":"Olivetti, N., Tiwari, A. (eds.): IJCAR. Vol. 9706 of LNCS. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1. ISBN 978-3-319-40228-4","DOI":"10.1007\/978-3-319-40229-1"},{"key":"9576_CR56","doi-asserted-by":"publisher","unstructured":"Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX, vol. 3702 of LNCS, pp. 245\u2013261. Springer (2005). https:\/\/doi.org\/10.1007\/11554554_19. ISBN 3-540-28931-3","DOI":"10.1007\/11554554_19"},{"key":"9576_CR57","doi-asserted-by":"publisher","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, vol. 5195 of LNCS, pp. 283\u2013291. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_23. ISBN 978-3-540-71069-1","DOI":"10.1007\/978-3-540-71070-7_23"},{"issue":"2\u20133","key":"9576_CR58","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.3233\/AIC-2010-0464","journal-title":"AI Commun."},{"key":"9576_CR59","doi-asserted-by":"publisher","unstructured":"Otten, J.: A non-clausal connection calculus. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX, vol. 6793 of LNCS, pp. 226\u2013241. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4_18. ISBN 978-3-642-22118-7","DOI":"10.1007\/978-3-642-22119-4_18"},{"key":"9576_CR60","doi-asserted-by":"publisher","unstructured":"Otten, J.: Mleancop: a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR, vol. 8562 of LNCS, pp. 269\u2013276. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_20. ISBN 978-3-319-08586-9","DOI":"10.1007\/978-3-319-08587-6_20"},{"key":"9576_CR61","doi-asserted-by":"publisher","unstructured":"Otten, J.: nanoCoP: a non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR, vol. 9706 of LNCS, pp. 302\u2013312. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_21. ISBN 978-3-319-40228-4","DOI":"10.1007\/978-3-319-40229-1_21"},{"issue":"1\u20132","key":"9576_CR62","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1\u20132), 139\u2013161 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00037-3","journal-title":"J. Symb. Comput."},{"issue":"3","key":"9576_CR63","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293\u2013304 (1986). https:\/\/doi.org\/10.1016\/S0747-7171(86)80028-1","journal-title":"J. Symb. Comput."},{"issue":"2","key":"9576_CR64","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975). https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","journal-title":"Theor. Comput. Sci."},{"key":"9576_CR65","doi-asserted-by":"crossref","unstructured":"Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1853\u20131964. Elsevier, MIT Press (2001). ISBN 0-444-50813-9","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"9576_CR66","unstructured":"Raths, T., Otten, J.: randoCoP: randomizing the proof search order in the connection calculus. In: Konev, B., Schmidt, R.A., Schulz, S. (eds.) PAAR, vol. 373 of CEUR Workshop Proceedings. CEUR-WS.org (2008). http:\/\/ceur-ws.org\/Vol-373\/paper-08.pdf"},{"issue":"1\u20133","key":"9576_CR67","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. J. Autom. Reason. 38(1\u20133), 261\u2013271 (2007). https:\/\/doi.org\/10.1007\/s10817-006-9060-z","journal-title":"J. Autom. Reason."},{"key":"9576_CR68","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","year":"2001","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier, Amsterdam (2001)"},{"key":"9576_CR69","doi-asserted-by":"publisher","unstructured":"Rosin, C.D.: Nested rollout policy adaptation for Monte Carlo tree search. In: Walsh, T. (ed.) IJCAI, pp. 649\u2013654. IJCAI\/AAAI (2011). https:\/\/doi.org\/10.5591\/978-1-57735-516-8\/IJCAI11-115. ISBN 978-1-57735-516-8","DOI":"10.5591\/978-1-57735-516-8\/IJCAI11-115"},{"key":"9576_CR70","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.knosys.2011.08.008","journal-title":"Knowl. Based Syst."},{"key":"9576_CR71","doi-asserted-by":"publisher","unstructured":"Schulz, S.: Learning search control knowledge for equational theorem proving. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI, vol. 2174 of LNCS, pp. 320\u2013334. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45422-5_23. ISBN 3-540-42612-4","DOI":"10.1007\/3-540-45422-5_23"},{"key":"9576_CR72","doi-asserted-by":"publisher","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) LPAR-19, vol. 8312 of LNCS, pp. 735\u2013743. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49. ISBN 978-3-642-45220-8","DOI":"10.1007\/978-3-642-45221-5_49"},{"issue":"7587","key":"9576_CR73","doi-asserted-by":"publisher","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.P., Leach, M., Kavukcuoglu, K., Graepel, T., Hassabis, D.: Mastering the game of Go with deep neural networks and tree search. Nature 529(7587), 484\u2013489 (2016). https:\/\/doi.org\/10.1038\/nature16961","journal-title":"Nature"},{"key":"9576_CR74","doi-asserted-by":"publisher","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, vol. 5170 of LNCS, pp. 28\u201332. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6. ISBN 978-3-540-71065-3","DOI":"10.1007\/978-3-540-71067-7_6"},{"issue":"1","key":"9576_CR75","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The 4th IJCAR automated theorem proving system competition\u2014CASC-J4. AI Commun. 22(1), 59\u201372 (2009). https:\/\/doi.org\/10.3233\/AIC-2009-0441","journal-title":"AI Commun."},{"issue":"4","key":"9576_CR76","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. Reason. 43(4), 337\u2013362 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9143-8","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9576_CR77","doi-asserted-by":"publisher","first-page":"75","DOI":"10.3233\/AIC-2010-0483","volume":"24","author":"G Sutcliffe","year":"2011","unstructured":"Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition\u2014CASC-J5. AI Commun. 24(1), 75\u201389 (2011). https:\/\/doi.org\/10.3233\/AIC-2010-0483","journal-title":"AI Commun."},{"issue":"5","key":"9576_CR78","doi-asserted-by":"publisher","first-page":"607","DOI":"10.3233\/AIC-160709","volume":"29","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition\u2014CASC-J8. AI Commun. 29(5), 607\u2013619 (2016). https:\/\/doi.org\/10.3233\/AIC-160709","journal-title":"AI Commun."},{"issue":"2","key":"9576_CR79","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition\u2014CASC. AI Mag. 37(2), 99\u2013101 (2016). https:\/\/doi.org\/10.1609\/aimag.v37i2.2620","journal-title":"AI Mag."},{"key":"9576_CR80","doi-asserted-by":"publisher","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483. Springer (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28. ISBN 978-3-642-81955-1","DOI":"10.1007\/978-3-642-81955-1_28"},{"issue":"3\u20134","key":"9576_CR81","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J Urban","year":"2004","unstructured":"Urban, J.: MPTP\u2014motivation, implementation, first experiments. J. Autom. Reason. 33(3\u20134), 319\u2013339 (2004). https:\/\/doi.org\/10.1007\/s10817-004-6245-1","journal-title":"J. Autom. Reason."},{"key":"9576_CR82","doi-asserted-by":"publisher","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, vol. 6327 of LNCS, pp. 155\u2013166. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15582-6_30. ISBN 978-3-642-15581-9","DOI":"10.1007\/978-3-642-15582-6_30"},{"key":"9576_CR83","doi-asserted-by":"publisher","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: MaLeCoP machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX, vol. 6793 of LNCS, pp. 263\u2013277. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4_21. ISBN 978-3-642-22118-7","DOI":"10.1007\/978-3-642-22119-4_21"},{"key":"9576_CR84","doi-asserted-by":"publisher","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1\u2014machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR, vol. 5195 of LNCS, pp. 441\u2013456. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_37. ISBN 978-3-540-71069-1","DOI":"10.1007\/978-3-540-71070-7_37"},{"issue":"3","key":"9576_CR85","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996). https:\/\/doi.org\/10.1007\/BF00252178","journal-title":"J. Autom. Reason."},{"key":"9576_CR86","doi-asserted-by":"publisher","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, vol. 5170 of LNCS, pp. 33\u201338. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7. ISBN 978-3-540-71065-3","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"9576_CR87","unstructured":"Whalen, D.: Holophrasm: a neural automated theorem prover for higher-order logic (2016). CoRR arXiv:1608.02644"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09576-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09576-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09576-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,4]],"date-time":"2021-09-04T23:23:11Z","timestamp":1630797791000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09576-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,5]]},"references-count":87,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,2]]}},"alternative-id":["9576"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09576-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,5]]},"assertion":[{"value":"10 April 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 July 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 September 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}