Converting the Suggested Upper Merged Ontology to Typed First-order Form
This work addresses the need for formalizing ontologies in typed logic for automated theorem proving, but it is incremental as it extends existing translations to handle explicit typing and numerical classes.
The authors tackled the problem of translating the Suggested Upper Merged Ontology (SUMO) to Typed First-order Form (TFF) with level 0 polymorphism, building on prior work to create a TPTP FOF translation for theorem provers like E and Vampire, and they provided open-source code and an example proof in Vampire.
We describe the translation of the Suggested Upper Merged Ontology (SUMO) to Typed First-order Form (TFF) with level 0 polymorphism. Building on our prior work to create a TPTP FOF translation of SUMO for use in the E and Vampire theorem provers, we detail the transformations required to handle an explicitly typed logic, and express SUMO's type hierarchy for numbers in a manner consistent with its intended semantics and the three numerical classes allowed in TFF. We provide description of the open source code and an example proof in Vampire on the resulting theory.