Adimen-SUMO is an off-the-shelf first-order ontology that has been obtained by reengineering out of the 88% of SUMO (Suggested Upper Merged Ontology). Adimen-SUMO can be used appropriately by FO theorem provers (like E-Prover or Vampire) for formal reasoning.

The contribution of Adimen-SUMO to the area of ontological formal reasoning is threefold. Firstly, we translated SUMO from its original format into the standard first order language. Secondly, we used first-order theorem provers as inference engines for debugging the ontology. Thus, we detected and repaired several significant problems with the axiomatization of the SUMO ontology. Problems we encountered include incorrectly defined axioms, redundancies, non-desirable properties, and axioms that do not produce expected logical consequences. Thirdly, as a result of the process of adapting the SUMO ontology, we discovered a basic design problem of the ontology which impedes its appropriate use with first order theorem provers. Consequently, we also propose a new transformation to overcome this limitation. As a result of this process, we obtain a validated first-order version of the ontology to be used by first-order theorem provers.

[2017/05] The last release of Adimen-SUMO v2.6: []

Related resources:

[2015/09] Adimen-SUMO portal.

[2015/09] Adimen-SUMO v2.4:

[2016/05] ATP system evaluation []

[2012/10] Adimen-SUMO v2.2: []


Alvez J., Lucio P. and Rigau G. Providing First-Order Reasoning Support to Large and Complex Ontologies. KYOTO Technical Report TR007/WP06. 2010.

Alvez J., Lucio P. and Rigau G. Adimen-SUMO: Reengineering an Ontology for First-Order Reasoning. International Journal on Semantic Web and Information Systems (IJSWIS). Volume 8 (4). IGI Global, USA. 2012.

Alvez J. Lucio P. and Rigau G. Improving the Competency of First-Order Ontologies. Proceedings of the 8th International Conference on Knowledge Capture (K-CAP 2015). Palisades, NY. 2015. [DOI] [Slides]

Alvez J. Lucio Pand Rigau G. Evaluating the Competency of a First-Order Ontology. Proceedings of the 8th International Conference on Knowledge Capture (K-CAP 2015). Palisades, NY. 2015. [DOI]

Alvez J. Lucio Pand Rigau G. Evaluating Automated Theorem Provers Using Adimen-SUMO. Proceedings of the 3rd Vampire Workshop at the 8th International Joint Conference on Automated Reasoning (IJCAR 2016). Coimbra. Portugal. 2016. [electronic edition @] ATP system evaluation: []

Alvez J. Hermo M., Lucio Pand Rigau G. Automatic White-Box Testing of First-Order Logic Ontologies. 2017. Electronic material: [[]

Alvez J. Lucio Pand Rigau G. Black-box Testing of First-Order Logic Ontologies Using WordNet. 2017.  Electronic material: [] []