Formal Modelling of Ontologies : An Event-B based Approach Using the Rodin Platform

TL;DR

This paper presents a formal approach to modeling ontologies using Event-B, enabling explicit domain knowledge representation and integration into design models via the Rodin platform.

Contribution

It introduces a novel method for formalizing ontologies as Event-B theories, facilitating their integration into design models with a rigorous formal foundation.

Findings

Ontologies are formalized as Event-B theories with sets, axioms, and theorems.

Ontologies are integrated into design models through an annotation mechanism.

The approach leverages the Rodin platform for formal modeling and reasoning.

Abstract

This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms, theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper, we particularly describe how ontologies are formalised as Event-B theories.