First order reasoning on a large ontology

Adam Pease, Geoff Sutcliffe

Research output: Contribution to journalConference articlepeer-review

18 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)61-70
Number of pages10
JournalCEUR Workshop Proceedings
StatePublished - Dec 1 2007
Event21st CADE 2007 Workshop on Empirically Successful Automated Reasoning in Large Theories, ESARLT 2007 - Bremen, Germany
Duration: Jul 17 2007Jul 17 2007

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'First order reasoning on a large ontology'. Together they form a unique fingerprint.

Cite this