Translating SUMO-K to Higher-Order Set Theory
Not on the map. Why?
Abstract (arXiv)
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 a very secure 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's 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 can be used to form a corpus of higher-order common-sense reasoning problems.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 9 of its 26 references that are in the map. First posted on arXiv 13 May 2023.
Builds on
9 of 26 references.
References · 9
- 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 52
- 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
- 2020ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)cited by 26
- 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
- 2019Hammering Mizar by Learning Clause Guidancecited by 20
- 2014Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Descriptioncited by 7
- 2022Lash 1.0 (System Description)cited by 4
- 2019A Tale of Two Set Theoriescited by 2
- 2023Converting the Suggested Upper Merged Ontology to Typed First-order Formcited by 1
Built on by
Not cited yet.