A method for evaluating and standardizing ontologies

The Open Biomedical Ontology (OBO) Foundry initiative is a collaborative effort for developing interoperable, science-based ontologies. The Basic Formal Ontology (BFO) serves as the upper ontology for the domain-level ontologies of OBO. BFO is an upper ontology of types as conceived by defenders of realism. Among the ontologies developed for OBO use, there are those which have been ratified, and those currently holding the status of candidate. To maintain consistency between ontologies, it is important to establish formal principled criteria that a candidate ontology must meet for ratification. Members of the OBO Foundry have expressed interest in using OntoClean to help construct BFO compliant domain ontologies. OntoClean is a system that decomposes the notion of sortal into criteria for deciding when subsumption can hold between classes. OntoClean primarily includes three components, based on the notions of Rigidity, Identity, and Unity. The methodology for integrating the OntoClean and BFO approaches to constructing consistent ontologies has been clarified by this dissertation. A formal integration between BFO, the Relation Ontology of BFO (RO), and OntoClean is given. The informal aspects and differing formalisms within and between the theories are analyzed and integrated within the axioms and theorems of one first-order system put forth in the dissertation. To set the foundation for this work, the categorical units of type and property of BFO and OntoClean, respectively, are unified under class. The modal logic axioms that OntoClean's theory of Rigidity is expressed within are interpreted and reformulated in our system, where axioms connecting it with BFO's categorical unit type is given. Central to this work is the axiom that a type is a class that is Rigid, i.e., a class whose definition is fundamental to the existence of the members of the class. A unity criterion for a class is a way in which certain parts of a member of the class are related such that they form the whole member. Our reformulation of this work focuses on the notion of the underlying unifying relation. As opposed to the informal approach taken by OntoClean, we express the notion that a class is unified under a relation as a meta-predicate defined by a definition schema. An identity criterion for a class is a test by which a member of the class can be re-identified. However as given in OntoClean, the notion of identity criteria is ontologically ambiguous. A formalization is given that provides a mapping to processes during which identity is confirmed. The reformulations of Unity and Identity are discussed in terms of Material Entity subtypes of BFO's theory. The integration work and resulting formal system affords a theoretically sound ontological foundation. A method for evaluating and standardizing candidate OBO Foundry ontologies is developed atop this foundation, where the method focuses on BFO's integration with OntoClean's notion of Rigidity. The method is given as a decision tree algorithm that evaluates one class at a time as they are introduced into an ontology, asking a prospective modeler questions that map to specific integration axioms. Finally, an implementation of the decision tree is provided in the form of an interactive Wizard plugin for the ontology editor Protégé. In an iterative approach informal user testing was applied to improve the questions and error messages. The plugin serves to facilitate ontologists and subject matter experts in making explicit what is implicit in, or unclearly specified for, the classes they choose to introduce into an ontology. Ultimately though, the integration axioms serves as a software platform-independent foundation for future software designed to evaluate and standardize candidate domain ontologies for the OBO Foundry