{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:50:59Z","timestamp":1743097859280,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031433689"},{"type":"electronic","value":"9783031433696"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe a translation from a fragment of SUMO (SUMO-K) into higher-order set theory. The translation provides a formal semantics for portions of SUMO which are beyond first-order and which have previously only had an informal interpretation. It also for the first time embeds a large common-sense ontology into an interactive theorem proving system. We further extend our previous work in finding contradictions in SUMO from first-order constructs to include a portion of SUMO\u2019s higher-order constructs. Finally, using the translation, we can create problems that can be proven using higher-order interactive and automated theorem provers. This is tested in several systems and used to form a corpus of higher-order common-sense reasoning problems.<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_14","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"255-274","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Translating SUMO-K to\u00a0Higher-Order Set Theory"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9772-1266","authenticated-orcid":false,"given":"Adam","family":"Pease","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1384-1613","authenticated-orcid":false,"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Pease, A.: Higher-Order Aspects and Context in SUMO. In: Jos Lehmann, I.J.V., Bundy, A. (eds.) Special issue on Reasoning with context in the Semantic Web, vol. 12\u201313. Science, Services and Agents on the World Wide Web (2012)","DOI":"10.1016\/j.websem.2011.11.008"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: Thf0 - the core of the tptp language for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, pp. 491\u2013506. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Brown, C.E., Kaliszyk, C.: Lash 1.0 (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8\u201310, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 350\u2013358. Springer (2022)","DOI":"10.1007\/978-3-031-10769-6_21"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Brown, C.E., P\u0105k, K.: A Tale of Two Set Theories. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 44\u201360. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_4","DOI":"10.1007\/978-3-030-23250-4_4"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Chvalovsk\u00fd, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In: Fontaine, P. (ed.) Automated Deduction - CADE 27\u201327th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11716, pp. 197\u2013215. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Chvalovsk\u00fd, K., Ols\u00e1k, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA anonymous: Symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12167, pp. 448\u2013463. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29","DOI":"10.1007\/978-3-030-51054-1_29"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17\u201321, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10383, pp. 292\u2013302. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6","DOI":"10.1007\/978-3-319-62075-6"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: Hammering Mizar by learning clause guidance. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019(September), pp. 9\u201312, 2019. Portland, OR, USA. LIPIcs, vol. 141, 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":"14_CR9","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Automating Formalization by Statistical and Semantic Parsing of Mathematics. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 12\u201327. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_2","DOI":"10.1007\/978-3-319-66107-0_2"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Learning to parse on aligned corpora (rough diamond). In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24\u201327, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9236, pp. 227\u2013233. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1","DOI":"10.1007\/978-3-319-22102-1"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J., Geuvers, H.: Developing corpus-based translation methods between informal and formal mathematics: Project description. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7\u201311, 2014. Proceedings. LNCS, vol. 8543, pp. 435\u2013439. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_34","DOI":"10.1007\/978-3-319-08434-3_34"},{"key":"14_CR12","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"14_CR13","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional calculi. Mathematical Logic Quarterly 9, 67\u201396 (1963). https:\/\/doi.org\/10.1002\/malq.19630090502","DOI":"10.1002\/malq.19630090502"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Niles, I., Pease, A.: Toward a Standard Upper Ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems (FOIS-2001). pp. 2\u20139 (2001)","DOI":"10.1145\/505168.505170"},{"key":"14_CR16","volume-title":"Ontology: A Practical Guide","author":"A Pease","year":"2011","unstructured":"Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin, CA (2011)"},{"key":"14_CR17","unstructured":"Pease, A.: Arithmetic and inference in a large theory. In: AI in Theorem Proving (2019)"},{"key":"14_CR18","unstructured":"Pease, A.: Converting the Suggested Upper Merged Ontology to Typed First-order Form arXiv:2303.04148 [cs.AI] (2023)"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Pease, A., Schulz, S.: Knowledge Engineering for Large Ontologies with Sigma KEE 3.0. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 519\u2013525. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_40","DOI":"10.1007\/978-3-319-08587-6_40"},{"issue":"2\u20133","key":"14_CR20","first-page":"137","volume":"23","author":"A Pease","year":"2010","unstructured":"Pease, A., Sutcliffe, G., Siegel, N., Trac, S.: Large Theory Reasoning with SUMO at CASC. AI Communications, Special issue on Practical Aspects of Automated Reasoning 23(2\u20133), 137\u2013144 (2010)","journal-title":"AI Communications, Special issue on Practical Aspects of Automated Reasoning"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Pease, A., Sutcliffe, G., Siegel, N., Trac, S.: Large theory reasoning with sumo at casc. AI Commun. 23(2\u20133), 137\u2013144 (2010). https:\/\/doi.org\/10.3233\/AIC-2010-0466","DOI":"10.3233\/AIC-2010-0466"},{"issue":"2\u20133","key":"14_CR22","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - A Brainiac Theorem Prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Schulz, S., Sutcliffe, G., Urban, J., Pease, A.: Detecting inconsistencies in large first-order knowledge bases. In: Proceedings of CADE 26. pp. 310\u2013325. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5_19"},{"key":"14_CR24","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover leo-iii. CoRR abs\/1802.02732 (2018), https:\/\/arxiv.org\/abs\/1802.02732"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Proceedings of the Second International Conference on Computer Science: Theory and Applications. pp. 6\u201322. CSR\u201907, Springer-Verlag, Berlin, Heidelberg (2007), https:\/\/dl.acm.org\/citation.cfm?id=2391910.2391914","DOI":"10.1007\/978-3-540-74510-5_4"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP Typed First-Order Form with Arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32","DOI":"10.1007\/978-3-642-28717-6_32"},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-79876-5_24","volume-title":"Automated Deduction - CADE 28","author":"P Vukmirovi\u0107","year":"2021","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28, pp. 415\u2013432. Springer International Publishing, Cham (2021)"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Wang, Q., Kaliszyk, C., Urban, J.: First Experiments with Neural Translation of Informal to Formal Mathematics. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 255\u2013270. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_22","DOI":"10.1007\/978-3-319-96812-4_22"}],"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-031-43369-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:34:51Z","timestamp":1694702091000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}