10 Outlook: Explanation

The RacerPro reasoning engine is currently being extended to provide explanations for unsatisfiable concepts, for subsumption relationships (either unwanted or unexpected), and for unsatisfiable Aboxes. An example for an unsatisfiable Abox is shown in the following example.

(in-knowledge-base test)  
 
(implies a b)  
(equivalent c (some r a))  
(equivalent d (some r b))  
 
(instance i (and c (not d)))  
 
(check-abox-coherence)

In Figure 13 it is indicated which axioms in the Tbox and which assertions in the Abox are the culprits for the inconsistency of the Abox. The figure shows a window from the development environment of RacerPro in order to demonstrate what will be provided in the near future with the next beta release. The explanation facilities will be integrated into RacerPorter and RacerEditor.


PIC

Figure 13: Explanation for an unsatisfiable Abox.


Explanation for query answering is already available (see above) in case a boolean query is answered with false but the expected answer is true. One can use the operator retrieve-with-explanation as described above. In the near future, this kind of explanation will also be integrated into the RacerPorter and RacerEditor environments as well.