First Order Reasoning on a Large Ontology

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.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Adam Pease, Geoff Sutcliffe
• Keywords: Automated Reasoning, CADE 2007, Order Format, Order Theorem, Upper Merged Ontology