FUB ORM2OWL Translator/Reasoner

From ONTORULE Show Case

Motivation

The ORM2 automated reasoning support tool is implemented in Java and includes:

• a parser for ORM2 Formal Syntax,
• a set of Java classes representing the ORM2 conceptual schema,
• a translator from ORM2 conceptual schema into OWL2 ontologies, and
• an ORM2 schema consistency check support exploiting existing reasoning engines (e.g. HermiT or FaCT++).

The workflow diagram of the tool is depicted on the picture.

Description

The tool provides the following functionality:

• Checking the consistency of a given ORM2 schema which may include both alethic (necessities and possibilities) and deontic (obligations and permissions) constraints. One of the advantages of the underlying approach is the straight-forward possibility to determine whether the inconsistency is caused purely by alethic or deontic constraints or by their combination. Additionally to the result of the consistency check, the tool prints out the list of concepts which are involved in conflicting constraints.
• Translating a given ORM2 schema into OWL2 ontology which can then be saved in various formats for further use. However, this translation does not support modalities in their diversity and, therefore, takes into account only structural constraints (i.e. alethic rules).

The graphical user interface of a tool is introduced in figure below: It allows to select an input file, underlying reasoner, output file, and output format for resulting ontology (if needed). The consistency check for an input ORM2 schema is performed after loading the input file and the result of the check is communicated by visual flag as well as by a detailed log in the corresponding window.

Automatic schema consistency check: An example.
In order to illustrate the functionality of the consistency check we will consider the ORM2 schema depicted in the figure.

The schema can be verbalised by means of the following set of conflicting business rules:

• Each car rental is insured by exactly one credit card
• Each luxury car rental is car rental
• It is obligatory that each luxury car rental is insured by at least two credit cards

The given set of constraints can be fully expressed in ALCQI description logic, therefore we can use the developed reasoning support tool for consistency check. The schema in the figure is internally inconsistent with respect to the third obligation since the latter clearly contradicts the first structural constraint which, together with is-a constraint on luxury car rental, simply does not support more than one credit card. Therefore, for any luxury car rental, the obligatory cardinality constraint cannot be satisfied. The same conclusion is indeed inferred by the implemented tool on the following figure.

References:

• Solomakhin, D.; Franconi, E.; and Mosca, A. 2011. Logic-based reasoning support for SBVR. In Proceedings of the 26th Italian Conference on Computational Logic (CILC2011), Pescara, Italy, 31 August 31-2 September 2011, number 810 in CEUR Workshop Proceedings. Aachen, Germany: Sun SITE Central Europe.
• Solomakhin, D. 2011. Logical Formalization of Semantic Business Vocabulary and Rules. MSc thesis, Faculty of Informatics, Vienna University of Technology.
• Franconi, E.; Mosca, A.; and Solomakhin, D. 2012. On the formalization of the ORM2 conceptual modelling language. 13th International Conference on Principles of Knowledge Representation and Reasoning (KR-2012). Submitted.