Verification of the Ontology of Professional Mathematics OntoMathPRO

We discuss our work on verifying the taxonomy of OntoMathPRO, an ontology of professional mathematical knowledge. Verification is based on methodologies of ontological modeling such as OntoClean. In line with these methodologies, we first formalize the identity conditions of the OntoMathPRO concepts. When a concept allows different conceptualizations, we explicate all of them, their pros and contras. Then we provide the concepts with metaontological annotations. Applying the constraints imposed by the identity conditions and metaontological annotations, we check the correctness of taxonomic relationships between concepts. Verification revealed several errors in the OntoMathPRO taxonomy, including incompatible identity conditions and confusion between subsumption, instantiation, and subtopic relations among others. We are going to correct the revealed inconsistencies and adopt the corrected taxonomy as a basis for developing the new version of the ontology, OntoMathPRO 2.0.