This document proposes as an extension to DIG 2.0 an interface to explanation inference services based on axiom pinpointing.
It has been argued in the literature [Debugging, Justifications] that standard inferences, like concept subsumption or satisfiability test, are insufficient in terms of pragmatic usage of a DL reasoner as a facility for ontology engineering. In fact, the ontology developer is likely to be a domain expert and often not an expert in logic. In this context, it is vital that the underlying reasoner be capable of debugging or, as a minimum requirement, explaining certain logical entailments it infers. The DIG 2.0 XML Schema for ASKs covers most of DL inferences recognized as standard, but it does not address the non-standard inference of explanation by means of axiom pinpointing. This document discusses what is needed and proposes syntax for such an interface.
<identifier/> request includes a new
element <explain> within the <ask> tag,
whenever the reasoner is capable of explanation.
This tag contains boolean ASK element for which explanation is supported.
An example for a reasoner identification:
<identifier
xmlns="http://dl.kr.org/dig/lang/schema"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://dl.kr.org/dig/lang/schema
http://dig.cs.manchester.ac.uk/schema.xsd"
name="CEL"
version="0.9b">
<supports>
<language>
[...]
</language>
<tell>
[...]
</tell>
<ask>
[...]
<explain>
<isSubClassOf/>
<isUnsatisfiable/>
<inconsistentKB/>
</explain>
</ask>
</supports>
</identifier>
asks request can now contain ask statements of type
explain. Each such a statement has an attribute id as
unique identification as other types of asks sub-elements. Nested
in each explain statement is an implication that needs to
be explained. We adopt the syntax of standard ask statements as
the syntax for the implications here as well.
The following is an example asks message comprising two
explain questions, both identified by IDs "q1" and
"q2" respectively.
<asks
xmlns="http://dl.kr.org/dig/lang/schema"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://dl.kr.org/dig/lang/schema
http://dig.cs.manchester.ac.uk/schema.xsd"
uri="'urn:uuid:...">
<explain id="q1">
<isSubClassOf>
<class name="Father"/>
<class name="Parent"/>
</isSubClassOf>
</explain>
<explain id="q2">
<isUnsatisfiable>
<class name="MotherWithoutChildren"/>
</isUnsatisfiable>
</explain>
</asks>
q1 asks for all explanations for the sub-class
relationship between Father and Parents, while
q1 asks for all explanations for the unsatisfiability of
the named class MotherWithoutChildren.
In many applications, however, only a single explanation or a few are required. Thus, it does not make much sense to request for all possible explanations because there are in the worse case exponentially many. The computation of all of them can take too long and may lead to unsatisfactory user experience. Though in the case that all explanations are needed, incremental computation and retrieval may help increase overall performance. See DIG 2.0 Proposal for an ABox Query Interface for a similar scenario where incremental retrieval of query results is desirable.
To this end, we add the argument nexp to the explain
tag to specify the number of explanations requested. The value can be any
natural number or "all", which is supposed to be the default
value. A small modification of
the above example illustrates the use of this new argument.
<asks
xmlns="http://dl.kr.org/dig/lang/schema"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://dl.kr.org/dig/lang/schema
http://dig.cs.manchester.ac.uk/schema.xsd"
uri="'urn:uuid:...">
<explain id="q3" nexp="1">
<isSubClassOf>
<class name="Father"/>
<class name="Parent"/>
</isSubClassOf>
</explain>
<explain id="q4" nexp="all">
<isUnsatisfiable>
<class name="MotherWithoutChildren"/>
</isUnsatisfiable>
</explain>
</asks>
In case of retrieval of the next/rest of the explanations to the question
requested previously, we use explain with the same id
as the previous one and without body. The following request asks for the next
explanation continuing from the previous q3 request.
<asks xmlns="http://dl.kr.org/dig/lang/schema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://dl.kr.org/dig/lang/schema http://dig.cs.manchester.ac.uk/schema.xsd" uri="'urn:uuid:..."> <explain id="q3" nexp="1"> </explain> </asks>Note that this is in conformance with the Proposal for ABox Query Interface.
explain request has an attribute
id which corresponds with the ID of the submitted ask
statement. It contains a number (at most as many as specified in
nexp of the request) of axioms statements (sets of
axioms).
Assume we have told the reasoner the following knowledge base:
<axioms
xmlns="http://dl.kr.org/dig/lang/schema"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://dl.kr.org/dig/lang/schema
http://dig.cs.manchester.ac.uk/schema.xsd"
<equivalentClass ID="ax01">
<class URI="Man"/>
<intersectionOf>
<class URI="Human"/>
<class URI="Male"/>
</intersectionOf>
</equivalentClass>
<equivalentClass ID="ax02">
<class URI="Woman"/>
<intersectionOf>
<class URI="Human"/>
<class URI="Female"/>
</intersectionOf>
</equivalentClass>
<equivalentClass ID="ax03">
<class URI="Parent"/>
<intersectionOf>
<class URI="Human"/>
<someValuesFrom>
<objectProperty URI="child"/>
<class URI="Human"/>
</someValuesFrom>
</intersectionOf>
</equivalentClass>
<equivalentClass ID="ax04">
<class URI="Father"/>
<intersectionOf>
<class URI="Man"/>
<someValuesFrom>
<objectProperty URI="child"/>
<class URI="Human"/>
</someValuesFrom>
</intersectionOf>
</equivalentClass>
<equivalentClass ID="ax05">
<class URI="Mother"/>
<intersectionOf>
<class URI="Woman"/>
<someValuesFrom>
<objectProperty URI="child"/>
<class URI="Human"/>
</someValuesFrom>
</intersectionOf>
</equivalentClass>
<equivalentClass ID="ax06">
<class URI="MotherWithoutChildren"/>
<intersectionOf>
<class URI="Mother"/>
<allValuesFrom>
<objectProperty URI="child"/>
<class URI="owl:Nothing"/>
</allValuesFrom>
</intersectionOf>
</equivalentClass>
<subClass ID="ax07">
<unionOf>
<class URI="Father"/>
<class URI="Mother"/>
</unionOf>
<class URI="Parent"/>
</subClass>
</axioms>
The response to the explanation request q1/q2 may
look like as follows.
<responses
xmlns="http://dl.kr.org/dig/lang/schema"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://dl.kr.org/dig/lang/schema
http://dig.cs.manchester.ac.uk/schema.xsd"
<explanations id="q1">
<axioms>
<axiom id="ax01"/>
<axiom id="ax03"/>
<axiom id="ax04"/>
</axioms>
<axioms>
<axiom id="ax07"/>
</axioms>
</explanations>
<explanations id="q2">
<axioms>
<axiom id="ax05"/>
<axiom id="ax06"/>
</axioms>
</explanations>
</responses>
The response to q3/q4 should be similar except that
the first explanations contains only one axioms,
either of the two is up to the reasoner. The other axioms should
be returned as the response of a subsequent explanation request. Of course, we
might also adopt the idea of notifier message here, but it should
be better defined, i.e. we should address what the possible messages are and
what the semantics is.