Abstract
Ontology-driven conceptual models are precise and semantically transparent domain descriptions that enable the development of information systems. As symbolic artefacts, such models are usually considered to be self-explanatory. However, the complexity of a system significantly correlates with the complexity of the conceptual model that describes it. Abstractions of both conceptual models and ontology-driven conceptual models are thus considered to be a promising way to improve the understandability and comprehensibility of those models. Although algorithms for providing abstractions of such models already exist, they still lack precisely formulated formal semantics. This paper aims to provide an approach towards the formalization of the abstraction process. We specify in first-order modal logic one of the graph-rewriting rules for ontology-driven conceptual model abstractions, in order to verify the correctness of the corresponding abstraction step. We also assess the entire network of abstractions of ontology-driven conceptual models and discuss existing drawbacks.