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.

Image ToolMenu
Figure 12: Connecting to a reasoner.
Image Connecting

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 Image submit bar button represents this menu item. Selecting one of them causes the following:

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

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.

Pablo Fillottrani 2010-08-17