{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:35Z","timestamp":1758979295687,"version":"3.41.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_24","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"349-361","source":"Crossref","is-referenced-by-count":17,"title":["Internal Guidance for Satallax"],"prefix":"10.1007","author":[{"given":"Michael","family":"F\u00e4rber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chad","family":"Brown","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"issue":"2\u20134","key":"24_CR1","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"24_CR3","unstructured":"Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Le Hoang, T., 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. CoRR, abs\/1501.02155 (2015)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Kennedy, J., Eberhart, R.: Particle swarm optimization. In: IEEE International Conference on Neural Networks, vol. 4, pp. 1942\u20131948, November 1995","DOI":"10.1109\/ICNN.1995.488968"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-319-21401-6_27","volume-title":"Automated Deduction - CADE-25","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Schulz, S., Urban, J., Vyskocil, J.: System description: E.T. 0.1. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS (LNAI), vol. 9195, pp. 389\u2013398. Springer, Heidelberg (2015)"},{"issue":"2","key":"24_CR7","doi-asserted-by":"crossref","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. Reasoning 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"24_CR8","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., et al. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 88\u201396. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_7"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"24_CR10","unstructured":"Daniel, A.K.: Machine learning for automated reasoning. Ph.D. thesis, Radboud Universiteit Nijmegen, April 2014"},{"key":"24_CR11","series-title":"lecture notes in computer science (lecture notes in artificial intelligence)","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/978-3-540-71070-7_23","volume-title":"Automated Reasoning","author":"J Otten","year":"2008","unstructured":"Otten, J.: $$\\sf leanCoP 2.0$$ and $$\\sf 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)"},{"issue":"1","key":"24_CR12","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1\u201327 (2010)","journal-title":"J. Formalized Reasoning"},{"issue":"1","key":"24_CR13","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.jal.2012.12.002","volume":"11","author":"N Sultana","year":"2013","unstructured":"Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II, Satallax on the Sledgehammer test bench. J. Appl. Logic 11(1), 91\u2013102 (2013)","journal-title":"J. Appl. Logic"},{"key":"24_CR14","unstructured":"Schulz, S.: Learning Search Control Knowledge for Equational Deduction. DISKI, vol. 230. Akademische Verlagsgesellschaft Aka GmbH Berlin, Berlin (2000)"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"24_CR16","doi-asserted-by":"crossref","unstructured":"Urban, J.: BliStr: the blind Strategy maker. In: Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.) GCAI 32015, Global Conference on Artificial Intelligence. EPiC Series in Computing, vol. 36, pp. 312\u2013319. EasyChair (2015)","DOI":"10.29007\/8n7m"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.: $$\\sf MaLeCoP$$ machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263\u2013277. Springer, Heidelberg (2011)"},{"issue":"3","key":"24_CR18","doi-asserted-by":"crossref","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. Reasoning 16(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:28:47Z","timestamp":1748986127000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}