# Translating SUMO-K to Higher-Order Set Theory

arXiv: https://arxiv.org/abs/2305.07903 · HTML: https://mlsanity.com/paper/2305.07903/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 26 references that are in the map.
- First posted on arXiv 13 May 2023.

## Builds on (most cited first, 9 of 9)

- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description](https://mlsanity.com/paper/1405.3451/) (2014)
- [Lash 1.0 (System Description)](https://mlsanity.com/paper/2205.06640/) (2022)
- [A Tale of Two Set Theories](https://mlsanity.com/paper/1907.08368/) (2019)
- [Converting the Suggested Upper Merged Ontology to Typed First-order Form](https://mlsanity.com/paper/2303.04148/) (2023)

## 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.