First order reasoning on a large ontology

Abstract

We present results of our work on using first order theorem proving to reason over a large ontology (the Suggested Upper Merged Ontology – SUMO), and methods for making SUMO suitable for first order theorem proving. We describe the methods for translating into standard first order format, as well as optimizations that are intended to improve inference performance. We also describe our work in translating SUMO from its native SUO-KIF language into TPTP format.