{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:18:05Z","timestamp":1758053885113,"version":"3.44.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>When humans evaluate the validity of a logical conclusion, they naturally consider its meaning and its context, allowing them to focus on relevant information and to avoid unnecessary inferences. For example, when asked to prove that all <jats:italic>hammocks<\/jats:italic> are also <jats:italic>beds<\/jats:italic>, they will certainly not draw conclusions about <jats:italic>vehicles<\/jats:italic> or <jats:italic>weapons<\/jats:italic>. In contrast, automated theorem provers typically do not account for the contextual meaning of a conclusion when selecting inference steps. Existing heuristics for selecting the clause for the next inference step usually ignore the meaning of symbol names, overlooking valuable contextual information. As a result, in the example above, clauses with symbol names such as <jats:italic>weapon<\/jats:italic> or <jats:italic>vehicle<\/jats:italic> could well be found in the processed clauses. However, since these clauses are not required for the actual proof, they are not helpful to the prover and tend to distract from the actual proof task. In this paper, we present an approach that uses natural language processing techniques to align the selection of the clause for the next inference step with the meaning of the proof goal. Our implementation and experimental results show that this method not only increases the number of successful proofs but also reduces the number of clauses processed during proof search.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_17","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:11Z","timestamp":1757887451000},"page":"306-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Context-Aware Clause Selection Using Symbol Name Meanings in\u00a0Theorem Proving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2455-0974","authenticated-orcid":false,"given":"Claudia","family":"Schon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"issue":"2","key":"17_CR1","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."},{"key":"17_CR2","unstructured":"\u00c1lvez, J., Hermo, M., Lucio, P., Rigau, G.: Automatic white-box testing of first-order logic ontologies. CoRR abs\/1705.10219 (2017). http:\/\/arxiv.org\/abs\/1705.10219"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"80","DOI":"10.4018\/jswis.2012100105","volume":"8","author":"J \u00c1lvez","year":"2012","unstructured":"\u00c1lvez, J., Lucio, P., Rigau, G.: Adimen-sumo: reengineering an ontology for first-order reasoning. Int. J. Semant. Web Inf. Syst. 8, 80\u2013116 (2012)","journal-title":"Int. J. Semant. Web Inf. Syst."},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek, F., Suda, M.: How much should this symbol weigh? A GNN-advised clause selection. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol.\u00a094, pp. 96\u2013111. EasyChair (2023). https:\/\/doi.org\/10.29007\/5F4R","DOI":"10.29007\/5F4R"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-61511-3_69","volume-title":"Automated Deduction \u2014 Cade-13","author":"J Denzinger","year":"1996","unstructured":"Denzinger, J., Schulz, S.: Learning domain knowledge to improve theorem proving. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 62\u201376. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_69"},{"key":"17_CR7","unstructured":"Firth, J.R.: Papers in Linguistics 1934\u20131951: Rep. Oxford University Press (1991)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-29436-6_15","volume-title":"Automated Deduction \u2013 CADE 27","author":"U Furbach","year":"2019","unstructured":"Furbach, U., Kr\u00e4mer, T., Schon, C.: Names are not just sound and smoke: word embeddings for axiom selection. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 250\u2013268. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_15"},{"key":"17_CR9","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., E\u00e9n, N., Chollet, F., Urban, J.: Deepmath - deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, Barcelona, Spain, pp. 2235\u20132243 (2016)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-62075-6_20","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2017","unstructured":"Jakub\u016fv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292\u2013302. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-96812-4_11","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2018","unstructured":"Jakub\u016fv, J., Urban, J.: Enhancing ENIGMA given clause guidance. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 118\u2013124. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_11"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: Hammering Mizar by learning clause guidance (short paper). In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, Portland, OR, USA, 9\u201312 September 2019. LIPIcs, vol.\u00a0141, pp. 34:1\u201334:8. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2019.34","DOI":"10.4230\/LIPICS.ITP.2019.34"},{"key":"17_CR13","unstructured":"Kahneman, D.: Thinking, Fast and Slow. Macmillan (2011)"},{"key":"17_CR14","unstructured":"Mikolov, T., Chen, K., Corrado, G., Dean, J.: Efficient estimation of word representations in vector space. CoRR abs\/1301.3781 (2013). http:\/\/arxiv.org\/abs\/1301.3781"},{"key":"17_CR15","unstructured":"Mikolov, T., Sutskever, I., Chen, K., Corrado, G.S., Dean, J.: Distributed representations of words and phrases and their compositionality. In: NIPS, pp. 3111\u20133119 (2013)"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Mikula, M., et al.: Magnushammer: a transformer-based approach to premise selection. CoRR abs\/2303.04488 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2303.04488","DOI":"10.48550\/ARXIV.2303.04488"},{"issue":"11","key":"17_CR17","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/219717.219748","volume":"38","author":"GA Miller","year":"1995","unstructured":"Miller, G.A.: WordNet: a lexical database for English. Commun. ACM 38(11), 39\u201341 (1995). https:\/\/doi.org\/10.1145\/219717.219748","journal-title":"Commun. ACM"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Miller, G.A., Charles, W.G.: Contextual correlates of semantic similarity. Lang. Cogn. Process. 6(1), 1\u201328 (1991). http:\/\/eric.ed.gov\/ERICWebPortal\/recordDetail?accno=EJ431389","DOI":"10.1080\/01690969108406936"},{"key":"17_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-031-70893-0_16","volume-title":"KI 2024","author":"O Jakobs","year":"2024","unstructured":"Jakobs, O., Schon, C.: Context-specific selection of commonsense knowledge using large language models. In: Hotho, A., Rudolph, S. (eds.) KI 2024. LNCS, vol. 14992, pp. 218\u2013231. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-70893-0_16"},{"key":"17_CR20","unstructured":"Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Piotrowski, B., Urban, J.: Stateful premise selection by recurrent neural networks. In: Albert, E., Kov\u00e1cs, L. (eds.) LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, 22\u201327 May 2020. EPiC Series in Computing, vol.\u00a073, pp. 409\u2013422. EasyChair (2020). https:\/\/doi.org\/10.29007\/J5HD","DOI":"10.29007\/J5HD"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-030-81097-9_6","volume-title":"Intelligent Computer Mathematics","author":"K Prorokovi\u0107","year":"2021","unstructured":"Prorokovi\u0107, K., Wand, M., Schmidhuber, J.: Improving stateful premise selection with transformers. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) CICM 2021. LNCS (LNAI), vol. 12833, pp. 84\u201389. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81097-9_6"},{"key":"17_CR23","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91\u2013110 (2002). http:\/\/content.iospress.com\/articles\/ai-communications\/aic259"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-46523-4_12","volume-title":"The Semantic Web \u2013 ISWC 2016","author":"S de Rooij","year":"2016","unstructured":"de Rooij, S., Beek, W., Bloem, P., van Harmelen, F., Schlobach, S.: Are names meaningful? Quantifying social meaning on the semantic web. In: Groth, P., et al. (eds.) ISWC 2016. LNCS, vol. 9981, pp. 184\u2013199. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46523-4_12"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Schon, C.: Selection strategies for commonsense knowledge (2022). https:\/\/doi.org\/10.48550\/ARXIV.2202.09163","DOI":"10.48550\/ARXIV.2202.09163"},{"key":"17_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-031-42608-7_14","volume-title":"KI 2023","author":"C Schon","year":"2023","unstructured":"Schon, C.: Associative reasoning for commonsense knowledge. In: Seipel, D., Steen, A. (eds.) KI 2023. LNCS, vol. 14236, pp. 170\u2013183. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-42608-7_14"},{"key":"17_CR27","unstructured":"Schon, C.: Using the meaning of symbol names to guide first-order logic reasoning. In: \u00d6z\u00e7ep, \u00d6.L., Ru\u00dfwinkel, N., Sauerwald, K., Wolter, D. (eds.) Proceedings of the 10th Workshop on Formal and Cognitive Reasoning co-located with the 47th German Conference on Artificial Intelligence (KI 2024), W\u00fcrzburg, Germany, 23 September 2024. CEUR Workshop Proceedings, vol.\u00a03763, pp. 19\u201327. CEUR-WS.org (2024). https:\/\/ceur-ws.org\/Vol-3763\/paper2.pdf"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-40229-1_23","volume-title":"Automated Reasoning","author":"S Schulz","year":"2016","unstructured":"Schulz, S., M\u00f6hrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 330\u2013345. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_23"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Speer, R., Chin, J., Havasi, C.: Conceptnet 5.5: an open multilingual graph of general knowledge. In: AAAI, pp. 4444\u20134451. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.11164"},{"issue":"3","key":"17_CR31","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.websem.2008.06.001","volume":"6","author":"FM Suchanek","year":"2008","unstructured":"Suchanek, F.M., Kasneci, G., Weikum, G.: YAGO: a large ontology from Wikipedia and WordNet. Web Semant. 6(3), 203\u2013217 (2008). https:\/\/doi.org\/10.1016\/j.websem.2008.06.001","journal-title":"Web Semant."},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-79876-5_31","volume-title":"Automated Deduction \u2013 CADE 28","author":"M Suda","year":"2021","unstructured":"Suda, M.: Improving ENIGMA-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 543\u2013561. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_31"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:14Z","timestamp":1757887454000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}