Name: JEFERSON DE OLIVEIRA BATISTA
Publication date: 25/03/2022
Advisor:
Name |
Role |
|---|---|
| JOÃO PAULO ANDRADE ALMEIDA | Advisor * |
Examining board:
| Name |
Role |
|---|---|
| JOÃO PAULO ANDRADE ALMEIDA | Advisor * |
| TIAGO PRINCE SALES | External Examiner * |
| VÍTOR ESTÊVÃO SILVA SOUZA | Internal Examiner * |
Summary: 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 well-
founded rules on the formation of taxonomic structures. The rigidity meta-property denes
whether a type applies essentially or contingently to its instances, while the sortality denes
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 dene 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 micro-
theories. 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 verication
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).
