Ontologically correct taxonomies by construction: a graph grammar-based approach
Nenhuma Miniatura disponível
Data
2022-03-25
Autores
Batista, Jeferson de Oliveira
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal do Espírito Santo
Resumo
Taxonomies play a central role in conceptual domain modeling, having a direct impact in areas such as knowledge representation, ontology engineering, and software engineering, as well as knowledge organization in information sciences. Despite this, there is little guidance on how to build high-quality taxonomies, with notable exceptions being the OntoClean methodology, and the ontology-driven conceptual modeling language OntoUML. These techniques take into account the ontological meta-properties of rigidity and sortality of types to establish wellfounded rules on the formation of taxonomic structures. The rigidity meta-property defines whether a type applies essentially or contingently to its instances, while the sortality defines whether a type provides a uniform principle of identity for its instances. In this dissertation, we show how to leverage the formal rules underlying these techniques in order to build taxonomies which are correct by construction. We define a set of correctness-preserving operations to systematically introduce types and subtyping relations into taxonomic structures. In addition to considering the ontological micro-theory of endurant types underlying OntoClean and OntoUML, we also employ the MLT (Multi-Level Theory) micro-theory of high-order types, which allows us to address multi-level taxonomies based on the powertype pattern, in which an entity can be both a type and an instance at the same time. To validate our proposal, we formalize the model building operations as a graph grammar that incorporates both microtheories. A graph grammar is a formal way to specify an initial graph and a set of graph transformation rules. Each graph represents a model, in our case, a taxonomy. A transformation rule consists of preconditions that must be true for a model in order to the rule be applicable, and a set of creation and deletion operations for vertices and edges. The set of models reachable applying the grammar rules is called the grammar language. We apply automatic verification techniques over the grammar language to show that the graph grammar is sound, i.e., that all taxonomies produced by the grammar rules are correct, at least up to a certain size. We also show that the rules can generate all correct taxonomies up to a certain size (a completeness result).
Descrição
Palavras-chave
Taxonomias , Modelagem conceitual , Ontologias , Gramáticas de grafo , Corretude por construção