{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:49:38Z","timestamp":1762325378251,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031107689"},{"type":"electronic","value":"9783031107696"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A<jats:italic>strategy schedule<\/jats:italic>allocates time to proof strategies that are used in sequence in a theorem prover. We employ Bayesian statistics to propose alternative sequences for the strategy schedule in each proof attempt. Tested on the TPTP problem library, our method yields a time saving of more than 50%. By extending this method to optimize the fixed time allocations to each strategy, we obtain a notable increase in the number of theorems proved.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_33","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"559-577","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Bayesian Ranking for\u00a0Strategy Scheduling in\u00a0Automated Theorem Provers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7600-1681","authenticated-orcid":false,"given":"Chaitanya","family":"Mangla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7979-1148","authenticated-orcid":false,"given":"Sean B.","family":"Holden","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"33_CR1","unstructured":"Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: Annual Conference on Neural Information Processing Systems, pp. 10338\u201310349 (2018)"},{"key":"33_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804779","volume-title":"Bayesian Reasoning and Machine Learning","author":"D Barber","year":"2012","unstructured":"Barber, D.: Bayesian Reasoning and Machine Learning. Cambridge University Press, Cambridge (2012)"},{"issue":"2","key":"33_CR3","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","volume":"53","author":"JP Bridge","year":"2014","unstructured":"Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving. J. Autom. Reas. 53(2), 141\u2013172 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9301-5","journal-title":"J. Autom. Reas."},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Cao, Z., Qin, T., Liu, T.Y., Tsai, M.F., Li, H.: Learning to rank: from pairwise approach to listwise approach. In: International Conference on Machine Learning, pp. 129\u2013136. Association for Computing Machinery (2007)","DOI":"10.1145\/1273496.1273513"},{"key":"33_CR5","unstructured":"Cheng, W., Dembczynski, K., H\u00fcllermeier, E.: Label ranking methods based on the Plackett-Luce model. In: International Conference on Machine Learning, pp. 215\u2013222. Omnipress (2010)"},{"key":"33_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/9781108671682","volume-title":"The Art of Feature Engineering: Essentials for Machine Learning","author":"P Duboue","year":"2020","unstructured":"Duboue, P.: The Art of Feature Engineering: Essentials for Machine Learning. Cambridge University Press, Cambridge (2020)"},{"key":"33_CR7","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of Intuitionism","author":"M Dummett","year":"2000","unstructured":"Dummett, M.: Elements of Intuitionism, 2nd edn. Clarendon, Oxford (2000)","edition":"2"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Guiver, J., Snelson, E.: Bayesian inference for Plackett-Luce ranking models. In: International Conference on Machine Learning, pp. 377\u2013384. Association for Computing Machinery (2009)","DOI":"10.1145\/1553374.1553423"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Hales, T., et al.: A formal proof of the Kepler conjecture. In: Forum of Mathematics, Pi, vol. 5 (2017)","DOI":"10.1017\/fmp.2017.1"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"H\u016fla, J., Moj\u017e\u00ed\u0161ek, D., Janota, M.: Graph neural networks for scheduling of SMT solvers. In: International Conference on Tools with Artificial Intelligence, pp. 447\u2013451 (2021)","DOI":"10.1109\/ICTAI52525.2021.00072"},{"key":"33_CR11","unstructured":"Johnson, S.R., Henderson, D.A., Boys, R.J.: On Bayesian inference for the Extended Plackett-Luce model (2020). arXiv:2002.05953"},{"key":"33_CR12","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Machine learner for automated reasoning 0.4 and 0.5 (2014). arXiv:1402.2359"},{"key":"33_CR13","unstructured":"Leyton-Brown, K., Nudelman, E., Andrew, G., McFadden, J., Shoham, Y.: A portfolio approach to algorithm selection. In: International Joint Conference on Artificial Intelligence, pp. 1542\u20131543. Morgan Kaufmann Publishers Inc. (2003)"},{"key":"33_CR14","volume-title":"Individual Choice Behavior: A Theoretical Analysis","author":"RD Luce","year":"1959","unstructured":"Luce, R.D.: Individual Choice Behavior: A Theoretical Analysis. Wiley, Hoboken (1959)"},{"key":"33_CR15","doi-asserted-by":"publisher","unstructured":"Mangla, C.: BRASS (2022). https:\/\/doi.org\/10.5281\/zenodo.6028568","DOI":"10.5281\/zenodo.6028568"},{"key":"33_CR16","volume-title":"Machine Learning: A Probabilistic Perspective","author":"KP Murphy","year":"2012","unstructured":"Murphy, K.P.: Machine Learning: A Probabilistic Perspective. MIT press, Cambridge (2012)"},{"key":"33_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0745-0","volume-title":"Bayesian Learning for Neural Networks","author":"RM Neal","year":"1996","unstructured":"Neal, R.M.: Bayesian Learning for Neural Networks. Springer, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4612-0745-0"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11554554_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Otten","year":"2005","unstructured":"Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 245\u2013261. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11554554_19"},{"key":"33_CR19","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). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_23"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-030-80223-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"N Pimpalkhare","year":"2021","unstructured":"Pimpalkhare, N., Mora, F., Polgreen, E., Seshia, S.A.: MedleySolver: online SMT algorithm selection. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 453\u2013470. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31"},{"issue":"2","key":"33_CR21","first-page":"193","volume":"24","author":"RL Plackett","year":"1975","unstructured":"Plackett, R.L.: The analysis of permutations. J. Roy. Stat. Soc. Ser. C (Appl. Stat.) 24(2), 193\u2013202 (1975)","journal-title":"J. Roy. Stat. Soc. Ser. C (Appl. Stat.)"},{"key":"33_CR22","series-title":"Adaptive Computation and Machine Learning","volume-title":"Gaussian Processes for Machine Learning","author":"CE Rasmussen","year":"2006","unstructured":"Rasmussen, C.E., Williams, C.K.I.: Gaussian Processes for Machine Learning. Adaptive Computation and Machine Learning, MIT Press, Cambridge (2006)"},{"issue":"6062","key":"33_CR23","doi-asserted-by":"publisher","first-page":"1518","DOI":"10.1126\/science.1205438","volume":"334","author":"DN Reshef","year":"2011","unstructured":"Reshef, D.N., et al.: Detecting novel associations in large data sets. Science 334(6062), 1518\u20131524 (2011)","journal-title":"Science"},{"issue":"4","key":"33_CR24","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1214\/ss\/1015346320","volume":"16","author":"GO Roberts","year":"2001","unstructured":"Roberts, G.O., Rosenthal, J.S.: Optimal scaling for various Metropolis-Hastings algorithms. Stat. Sci. 16(4), 351\u2013367 (2001)","journal-title":"Stat. Sci."},{"key":"33_CR25","volume-title":"Bayesian Statistics and Marketing","author":"PE Rossi","year":"2006","unstructured":"Rossi, P.E.: Bayesian Statistics and Marketing. Wiley, Hoboken (2006)"},{"issue":"5","key":"33_CR26","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1007\/s10994-017-5694-9","volume":"107","author":"D Sch\u00e4fer","year":"2018","unstructured":"Sch\u00e4fer, D., H\u00fcllermeier, E.: Dyad ranking using Plackett-Luce models based on joint feature representations. Mach. Learn. 107(5), 903\u2013941 (2018)","journal-title":"Mach. Learn."},{"issue":"23","key":"33_CR27","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a Brainiac Theorem Prover. AI Commun. 15(23), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"33_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-030-72013-1_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Scott","year":"2021","unstructured":"Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: MachSMT: a machine learning-based algorithm selector for SMT solvers. In: TACAS 2021. LNCS, vol. 12652, pp. 303\u2013325. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16"},{"issue":"1","key":"33_CR29","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1109\/JPROC.2015.2494218","volume":"104","author":"B Shahriari","year":"2015","unstructured":"Shahriari, B., Swersky, K., Wang, Z., Adams, R.P., De Freitas, N.: Taking the human out of the loop: a review of Bayesian optimization. Proc. IEEE 104(1), 148\u2013175 (2015)","journal-title":"Proc. IEEE"},{"key":"33_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809682","volume-title":"Kernel Methods for Pattern Analysis","author":"J Shawe-Taylor","year":"2004","unstructured":"Shawe-Taylor, J.: Kernel Methods for Pattern Analysis. Cambridge University Press, Cambridge (2004)"},{"key":"33_CR31","doi-asserted-by":"crossref","unstructured":"Silverthorn, B., Miikkulainen, R.: Latent class models for algorithm portfolio methods. In: AAAI Conference on Artificial Intelligence, pp. 167\u2013172. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7546"},{"issue":"4","key":"33_CR32","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v.6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"33_CR33","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. Reason. 18(2), 199\u2013204 (1997)","journal-title":"J. Autom. Reason."},{"key":"33_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-61291-2_65","volume-title":"Advances in Artifical Intelligence","author":"C Thornton","year":"1996","unstructured":"Thornton, C.: Parity: the problem that won\u2019t go away. In: McCalla, G. (ed.) AI 1996. LNCS, vol. 1081, pp. 362\u2013374. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61291-2_65"},{"key":"33_CR35","first-page":"211","volume":"1","author":"ME Tipping","year":"2001","unstructured":"Tipping, M.E.: Sparse Bayesian learning and the relevance vector machine. J. Mach. Learn. Res. 1, 211\u2013244 (2001)","journal-title":"J. Mach. Learn. Res."},{"key":"33_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-27984-9","volume-title":"MATLAB\u00ae Recipes for Earth Sciences","author":"MH Trauth","year":"2021","unstructured":"Trauth, M.H.: MATLAB\u00ae Recipes for Earth Sciences. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/3-540-27984-9"},{"key":"33_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292\u2013297. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_26"},{"key":"33_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-21736-9","volume-title":"All of Statistics: A Concise Course in Statistical Inference","author":"L Wasserman","year":"2004","unstructured":"Wasserman, L.: All of Statistics: A Concise Course in Statistical Inference. Springer, New York (2004). https:\/\/doi.org\/10.1007\/978-0-387-21736-9"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,25]],"date-time":"2023-11-25T05:22:18Z","timestamp":1700889738000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}