{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:12:36Z","timestamp":1773655956991,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,2,22]],"date-time":"2014-02-22T00:00:00Z","timestamp":1393027200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10817-014-9301-5","type":"journal-article","created":{"date-parts":[[2014,2,21]],"date-time":"2014-02-21T14:29:34Z","timestamp":1392992974000},"page":"141-172","source":"Crossref","is-referenced-by-count":48,"title":["Machine Learning for First-Order Theorem Proving"],"prefix":"10.1007","volume":"53","author":[{"given":"James P.","family":"Bridge","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sean B.","family":"Holden","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,22]]},"reference":[{"key":"9301_CR1","unstructured":"Bache, K., Lichman, M.: UCI Machine Learning Repository (2013). http:\/\/archive.ics.uci.edu\/ml"},{"issue":"5","key":"9301_CR2","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1093\/bioinformatics\/16.5.412","volume":"16","author":"P Baldi","year":"2000","unstructured":"Baldi, P., Brunak, S., Chauvin, Y., Anderson, C.A.F., Nielsen, H.: Assessing the accuracy of prediction algorithms for classification: an overview. Bioinformatics 16(5), 412\u2013424 (2000)","journal-title":"Bioinformatics"},{"key":"9301_CR3","unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning. Springer-Verlag (2006)"},{"key":"9301_CR4","unstructured":"Bridge, J.P.: Machine Learning and Automated Theorem Proving. Tech. Rep. UCAM-CL-TR-792, University of Cambridge, Computer Laboratory (2010). http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-792.pdf"},{"issue":"16","key":"9301_CR5","doi-asserted-by":"crossref","first-page":"3385","DOI":"10.1093\/bioinformatics\/bti526","volume":"21","author":"W Chu","year":"2005","unstructured":"Chu, W., Ghahramani, Z., Falciani, F., Wild, D.L.: Biomarker discovery in microarray gene expression data with Gaussian processes. Bioinformatics 21(16), 3385\u20133393 (2005)","journal-title":"Bioinformatics"},{"issue":"7","key":"9301_CR6","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). doi: 10.1145\/368273.368557","journal-title":"Commun. ACM"},{"issue":"3","key":"9301_CR7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). doi: 10.1145\/321033.321034","journal-title":"J. ACM"},{"key":"9301_CR8","unstructured":"Denzinger, J., Fuchs, M., Fuchs, M.: High performance ATP systems by combining several AI methods. In: Proceedings Fifteenth International Joint Conference on Artificial Intelligence (IJCAI) 1997, pp. 102\u2013107. Morgan Kaufmann (1997)"},{"key":"9301_CR9","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":"9301_CR10","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: Discount - a distributed and learning equational prover. J. Autom. Reason. 18, 189\u2013198 (1997). doi: 10.1023\/A:1005879229581","journal-title":"J. Autom. Reason."},{"key":"9301_CR11","unstructured":"Duda, R.O., Hart, P.E., Stork, D.G.: Pattern Classification, 2nd edn. Wiley (2000)"},{"key":"9301_CR12","unstructured":"Erkek, C.A.: Mixture of Experts Learning in Automated Theorem Proving. Master\u2019s thesis, Bogazici University (2010)"},{"key":"9301_CR13","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1016\/j.patrec.2005.10.010","volume":"27","author":"T Fawcett","year":"2006","unstructured":"Fawcett, T.: An introduction to ROC analysis. Pattern Recogn. Lett. 27, 861\u2013874 (2006)","journal-title":"Pattern Recogn. Lett."},{"key":"9301_CR14","unstructured":"Fuchs, M.: Automatic selection of search-guiding heuristics for theorem proving. In: Proceedings of the 10th FLAIRS, pp. 1\u20135. Florida AI Research Society, Daytona Beach (1998)"},{"issue":"3\u20134","key":"9301_CR15","first-page":"175","volume":"11","author":"M Fuchs","year":"1998","unstructured":"Fuchs, M., Fuchs, M.: Feature-based learning of search-guiding heuristics for theorem proving. AI Commun. 11(3\u20134), 175\u2013189 (1998)","journal-title":"AI Commun."},{"key":"9301_CR16","unstructured":"Goller, C.: Learning search-control heuristics for automated deduction systems with folding architecture networks. In: Proceedings European Symposium on Artificial Neural Networks. D-Facto publications (1999)"},{"key":"9301_CR17","doi-asserted-by":"crossref","unstructured":"Grimmett, G., Stirzaker, D.: Probability and Random Processes. Oxford University Press (2001)","DOI":"10.1093\/oso\/9780198572237.001.0001"},{"key":"9301_CR18","first-page":"1157","volume":"3","author":"I Guyon","year":"2003","unstructured":"Guyon, I., Elisseeff, A.: An introduction to variable and feature selection. J. Mach. Learn. Res. 3, 1157\u20131182 (2003)","journal-title":"J. Mach. Learn. Res."},{"key":"9301_CR19","doi-asserted-by":"crossref","unstructured":"Haim, S., Walsh, T.: Online estimation of SAT solving runtime. In: Kleine B\u00fcning, H., Zhao, X. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2008, Lecture Notes in Computer Science, vol. 4996, pp. 133\u2013138. Springer, Berlin (2008). doi: 10.1007\/978-3-540-79719-7_12","DOI":"10.1007\/978-3-540-79719-7_12"},{"key":"9301_CR20","doi-asserted-by":"crossref","unstructured":"Haim, S., Walsh, T.: Restart strategy selection using machine learning techniques. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009, Lecture Notes in Computer Science, vol. 5584, pp. 312\u2013325. Springer, Berlin (2009). doi: 10.1007\/978-3-642-02777-2_30","DOI":"10.1007\/978-3-642-02777-2_30"},{"key":"9301_CR21","doi-asserted-by":"crossref","unstructured":"Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning. Springer Series in Statistics, 2nd edn. Springer (2009)","DOI":"10.1007\/978-0-387-84858-7"},{"issue":"9","key":"9301_CR22","doi-asserted-by":"crossref","first-page":"1263","DOI":"10.1109\/TKDE.2008.239","volume":"21","author":"H He","year":"2009","unstructured":"He, H.: Learning from imbalanced data. IEEE Trans. Knowl. Data Eng. 21(9), 1263\u20131284 (2009)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"9301_CR23","unstructured":"Hsu, C.W., Chang, C.C., Lin, C.J., et al.: A practical guide to support vector classification. Tech. rep., Department of Computer Science, National Taiwan University (2003)"},{"key":"9301_CR24","doi-asserted-by":"crossref","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press (2004)","DOI":"10.1017\/CBO9780511810275"},{"key":"9301_CR25","unstructured":"Joachims, T.: Making large-scale SVM learning practical. In: Sch\u00f6lkopf, B., Burges, C., Smola, A. (eds.) Advances in Kernel Methods - Support Vector Learning, chap. 11, pp. 169\u2013184. MIT Press, Cambridge, MA (1999)"},{"key":"9301_CR26","doi-asserted-by":"crossref","unstructured":"Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Lee, J. (ed.) Principles and Practice of Constraint Programming \u2013 CP 2011, Lecture Notes in Computer Science, vol. 6876, pp. 454\u2013469. Springer, Berlin (2011). doi: 10.1007\/978-3-642-23786-7_35","DOI":"10.1007\/978-3-642-23786-7_35"},{"key":"9301_CR27","unstructured":"Kohavi, R.: A study of cross-validation and bootstrap for accuracy estimation and model selection. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI\u201995), vol. 2, pp. 1137\u20131143. Morgan Kaufmann (1995)"},{"issue":"16","key":"9301_CR28","doi-asserted-by":"crossref","first-page":"2626","DOI":"10.1093\/bioinformatics\/bth294","volume":"20","author":"GRG Lanckriet","year":"2004","unstructured":"Lanckriet, G.R.G., Bie, T.D., Cristianini, N., Jordan, M.I., Noble, W.S.: A statistical framework for genomic data fusion. Bioinformatics 20(16), 2626\u20132635 (2004)","journal-title":"Bioinformatics"},{"key":"9301_CR29","unstructured":"Luenberger, D.G.: Linear and Nonlinear Programming. Kluwer (2003)"},{"key":"9301_CR30","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"9301_CR31","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1098\/rsta.1909.0016","volume":"209","author":"J Mercer","year":"1909","unstructured":"Mercer, J.: Functions of positive and negative type and their connection with the theory of integral equations. Philos. Trans. R. Soc. Lond. 209, 415\u2013446 (1909)","journal-title":"Philos. Trans. R. Soc. Lond."},{"key":"9301_CR32","unstructured":"Mitchell, T.: Machine Learning. McGraw Hill (1997)"},{"key":"9301_CR33","unstructured":"Morik, K., Brockhausen, P., Joachims, T.: Combining statistical learning with a knowledge-based approach \u2013 a case study in intensive care monitoring. In: International Conference on Machine Learning (ICML), pp. 268\u2013277. Bled, Slowenien (1999)"},{"key":"9301_CR34","doi-asserted-by":"crossref","unstructured":"Nudelman, E., Leyton-Brown, K., Hoos, H., Devkar, A., Shoham, Y.: Understanding random SAT: Beyond the clauses-to-variables ratio. In: Wallace, M. (ed.) Principles and Practice of Constraint Programming \u2013 CP 2004, Lecture Notes in Computer Science, vol. 3258, pp. 438\u2013452. Springer, Berlin (2004). doi: 10.1007\/978-3-540-30201-8_33","DOI":"10.1007\/978-3-540-30201-8_33"},{"issue":"3\u20134","key":"9301_CR35","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1002\/minf.201100146","volume":"31","author":"NCV Pilkington","year":"2012","unstructured":"Pilkington, N.C.V., Trotter, M.W.B., Holden, S.B.: Multiple kernel learning for drug discovery. Mol. Inform. 31(3\u20134), 313\u2013322 (2012)","journal-title":"Mol. Inform."},{"key":"9301_CR36","doi-asserted-by":"crossref","unstructured":"Rasmussen, C.E., Williams, C.KI.: Gaussian Processes for Machine Learning. Adaptive Computation and Machine Learning. MIT Press, Cambridge, MA (2006)","DOI":"10.7551\/mitpress\/3206.001.0001"},{"key":"9301_CR37","doi-asserted-by":"crossref","unstructured":"Rosenblatt, F.: Principles of Neurodynamics: Perceptrons and the Theory of Brain Mechanisms. Spartan Books (1962)","DOI":"10.21236\/AD0256582"},{"key":"9301_CR38","unstructured":"Samulowitz, H., Memisevic, R.: Learning to solve QBF. In: Proceedings of the 22nd National Conference on Artificial Intelligence - AAAI\u201907, vol. 1, pp. 255\u2013260. AAAI Press (2007). http:\/\/dl.acm.org\/citation.cfm?id=1619645.1619686"},{"key":"9301_CR39","unstructured":"Schulz, S.: Learning Search Control Knowledge for Equational Deduction. No. 230 in DISKI. Akademische Verlagsgesellschaft Aka GmbH Berlin (2000)"},{"issue":"2\/3","key":"9301_CR40","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 a brainiac theorem prover. AI Commun. 15(2\/3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9301_CR41","doi-asserted-by":"crossref","unstructured":"Shawe-Taylor, J., Cristianini, N.: Support Vector Machines and Other Kernel-Based Learning Methods. Cambridge University Press, Cambridge (2000)","DOI":"10.1017\/CBO9780511801389"},{"key":"9301_CR42","doi-asserted-by":"crossref","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, Cambridge (2004)","DOI":"10.1017\/CBO9780511809682"},{"issue":"4","key":"9301_CR43","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: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9301_CR44","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/TKDE.2002.1000348","volume":"14","author":"KM Ting","year":"2002","unstructured":"Ting, K.M.: An instance-weighted method to induce cost-sensitive trees. IEEE Trans. Knowl. Data Eng. 14(3), 659\u2013665 (2002)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"9301_CR45","unstructured":"Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, no. 257 in CEUR Workshop Proceedings, pp. 45\u201358 (2007)"},{"issue":"12","key":"9301_CR46","doi-asserted-by":"crossref","first-page":"1342","DOI":"10.1109\/34.735807","volume":"20","author":"CKI Williams","year":"1998","unstructured":"Williams, C.KI., Barber, D.: Bayesian classification with Gaussian processes. IEEE Trans Pattern. Anal. Mach. Intell. 20(12), 1342\u20131351 (1998)","journal-title":"IEEE Trans Pattern. Anal. Mach. Intell."},{"key":"9301_CR47","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008)","journal-title":"J. Artif. Intell. Res."},{"key":"9301_CR48","unstructured":"Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: Features for SAT (2012). Available at www.cs.ubc.ca\/labs\/beta\/Projects\/SATzilla\/"},{"key":"9301_CR49","unstructured":"Xu, L., Hutter, F., Shen, J., Hoos, H., Leyton-Brown, K.: Satzilla2012: improved algorithm slection based on cost-sensitive classification models. In: Balint, A., Belov, A., Diepold, D., Gerber, S., J\u00e4rvisalo, M., Sinz, C. (eds.) Proceedings of SAT Challange 2012: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2012-2, pp. 57\u201358. University of Helsinki (2012)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9301-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9301-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9301-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,24]],"date-time":"2024-05-24T12:55:22Z","timestamp":1716555322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9301-5"}},"subtitle":["Learning to Select a Good Heuristic"],"short-title":[],"issued":{"date-parts":[[2014,2,22]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["9301"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9301-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2,22]]}}}