Reasoning

ICOM can be used as standalone schema editor. In order to use ICOM's reasoning capabilities, a Description Logic reasoner must be running. The Tool menu (shown in figure ) handles the communication with the reasoner.

Figure 12: Connecting to a reasoner.

ICOM provides a connection with the Description Logic reasoner that allows satisfiability checking of schemas and discovery of implied subsumptions. This connection is made via the HTTP protocol using the DIG syntax. When the connect to a reasoner menu item is selected, a dialog appear prompting for host and port information (see figure 12)

Once connected, the "Verify project" Tool menu item will become active. Alternatively, the bar button represents this menu item. Selecting one of them causes the following:

• the current project is translated to Description Logic by ICOM. Then this is transmitted to the reasoner.
• each class and association in the project is checked for satisfiability.
• for each class and association in the project, its equivalent peers, and super-classes (according to the classifier) are determined.
• for each class-role-association triple, check its stricter minimum and maximum cardinality.

After the verification process, several modifications to the schemas may be observed:

• all unsatisfiable items will appear in red in the schemas. An unsatisfiable item means that the item describes an empty set of instances and can never have any instances.
• several additional implications will appear in green:
  • all deduced semantically equivalent objects are connected with equivalent axiom links.
  • all deduced inclusive relationships between objects are connected with subsumption axiom links.
  • all roles whose cardinalities are determined more restrictive than originally specified.

Finally, in the status bar, you will see a line that reads either: ``Project is satisfiable", ``Project contains some unsatisfiable term'', or ``Project is unsatisfiable". This indicates the overall validity of the project.

At this point, if we elect to Discard deductions, by selecting the respective Tool menu item, the entire project will be returned to its original state (and any information about unsatisfiability will be discarded). Performing another schema edit will also discard the deductions before the editing is carried out. Alternatively, the equivalence, subsumption relation, and role cardinality deductions can be added permanently to the project through Commit deductions, using the Tool menu item. There is currently no undo function, while to undo Discard deductions is simply to redo the reasoning, there isn't an undo equivalent for Commit deductions, so always save your schemas/projects regularly.