{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T06:56:50Z","timestamp":1758265010096},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642344800"},{"type":"electronic","value":"9783642344817"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34481-7_82","type":"book-chapter","created":{"date-parts":[[2012,11,5]],"date-time":"2012-11-05T03:40:34Z","timestamp":1352086834000},"page":"673-682","source":"Crossref","is-referenced-by-count":2,"title":["Machine Learning Approach to Enhance the Design of Automated Theorem Provers"],"prefix":"10.1007","author":[{"given":"Mahdi","family":"Khalifa","sequence":"first","affiliation":[]},{"given":"Hazem","family":"Raafat","sequence":"additional","affiliation":[]},{"given":"Mohammed","family":"Almulla","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"82_CR1","unstructured":"Sutcliffe, G., Fuchs, M., Suttner, C.: Progress in Automated Theorem Proving 1997-1999. In: Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence (2001)"},{"key":"82_CR2","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G. Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating General Purpose Automated Theorem Proving Systems. Artificial Intelligence Journal\u00a0131, 39\u201354 (2001)","journal-title":"Artificial Intelligence Journal"},{"key":"82_CR3","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. Journal of Automated Reasoning\u00a08, 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"82_CR4","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. Journal of Automated Reasoning\u00a018(2), 199\u2013204 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"82_CR5","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of Vampire. Journal of Automated Reasoning\u00a015, 237\u2013265 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"82_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-48660-7_34","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topi\u0107, D.: System Description: Spass Version 1.0.0. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 378\u2013382. Springer, Heidelberg (1999)"},{"key":"82_CR7","first-page":"127","volume":"15","author":"B. L\u00f6chner","year":"2002","unstructured":"L\u00f6chner, B., Hillenbrand, T.: A Phytography of WALDMEISTER 1. AI Communications\u00a015, 127\u2013133 (2002)","journal-title":"AI Communications"},{"key":"82_CR8","unstructured":"Claessen, K., Sorensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: CADE-19 Workshop: Model Computation - Principles; Algorithms; and Applications (2003)"},{"key":"82_CR9","unstructured":"Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: 1st International Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics, pp. 56\u201368 (2003)"},{"issue":"4","key":"82_CR10","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"P. Andrews","year":"2006","unstructured":"Andrews, P., Brown, C.: TPS: A Hybrid Automatic-Interactive System for Developing Proofs. Journal of Applied Logic\u00a04(4), 367\u2013395 (2006)","journal-title":"Journal of Applied Logic"},{"key":"82_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Automated Deduction - CADE-15","author":"C.E. Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C.E., Kohlhase, M.: System Description: Leo - A Higher-Order Theorem Prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 139\u2013143. Springer, Heidelberg (1998)"},{"key":"82_CR12","first-page":"79","volume":"15","author":"F.J. Pelletier","year":"2002","unstructured":"Pelletier, F.J., Sutcliffe, G., Suttner, C.: The Development of CASC. AI Communications\u00a015, 79\u201390 (2002)","journal-title":"AI Communications"},{"issue":"2","key":"82_CR13","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"82_CR14","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/AIC-2010-0469","volume":"23","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The CADE-22 Automated Theorem Proving System Competition -CASC-22. AI Communications\u00a023, 47\u201360 (2010)","journal-title":"AI Communications"},{"key":"82_CR15","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.3 Reference Manual, Argonne National Laboratory, ANL\/MSC-TM-263 (2003)","DOI":"10.2172\/822573"},{"key":"82_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"82_CR17","unstructured":"Sutcliffe, G., Fuchs, M.: Homogeneous Sets of ATP Problems. In: 15th International Florida Artificial Intelligence Research Society Conference, pp. 57\u201361 (2000)"},{"key":"82_CR18","unstructured":"Denzinger, J., Fuchs, M.: High Performance ATP Systems by Combining Several AI Methods. In: 15th International Joint Conference on Artificial Intelligence, pp. 102\u2013107 (1997)"},{"key":"82_CR19","unstructured":"Fuchs, M.: A Feature-Based Learning Method for Theorem Proving. In: 15th National Conference on Artificial Intelligence, pp. 457\u2013462 (1998)"},{"key":"82_CR20","unstructured":"Kakkad, A.: Machine Learning for Automated Theorem Proving, unpublished Master\u2019s Thesis for Master\u2019s Degree, University of Miami (2009)"},{"issue":"2\/3","key":"82_CR21","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E- A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"issue":"4","key":"82_CR22","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Robinson, G., Carson, D.: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. Journal of the ACM\u00a012(4), 536\u2013541 (1965)","journal-title":"Journal of the ACM"},{"key":"82_CR23","unstructured":"Stenz, G., Wolf, A.: Strategy Selection by Genetic Programming. In: 12th International Florida Artificial Intelligence Research Society Conference, pp. 346\u2013350 (1999)"},{"key":"82_CR24","unstructured":"Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: 12th International Florida Artificial Intelligence Research Society Conference, pp. 341\u2013345 (1999)"},{"key":"82_CR25","first-page":"13","volume":"5","author":"C. Shearer","year":"2000","unstructured":"Shearer, C.: The CRISP-DM model: The New Blueprint for Data Mining. J. Data Warehousing\u00a05, 13\u201322 (2000)","journal-title":"J. Data Warehousing"},{"key":"82_CR26","unstructured":"Witten, H., Frank, E.: Data Mining: Practical Machine Learning Tools and Techniques, 2nd edn. Morgan Kaufmann (2005)"},{"issue":"2","key":"82_CR27","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s10817-004-3243-2","volume":"33","author":"M. Newborn","year":"2004","unstructured":"Newborn, M., Wang, Z.: Octopus: Combining Learning and Parallel Search. Journal of Automated Reasoning\u00a033(2), 171\u2013218 (2004)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Neural Information Processing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34481-7_82.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T08:55:19Z","timestamp":1620118519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34481-7_82"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642344800","9783642344817"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34481-7_82","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}