Proposed change to the OWL-2 Direct Semantics entailment regime

Hi,
I'd like to propose a change to the OWL-2 Direct Semantics entailment regime as it is currently defined in the spec.

Currently, bnodes in a BGP bind only to individuals or other bnodes. According to the formal semantics (and the spirit) of RDF, bnodes represent existential (but unknown) information. If the information is encoded in RDF (or in other simple languages where existential information can always be uniquely and exactly materialised explicitly as bnodes, like RDFS and OWL-RL) then the existential meaning of bnodes in queries is correctly captured by binding them just to individuals or other bnodes. However, in OWL-2 Direct Semantics entailment regime a lot of existential information remain necessarily implicit, and we would weaken the notion of answer (wrt standard OWL-2 Direct Semantics entailment regime in 25 years of description logics literature) if we do not treat bnodes in BGPs properly.

Let me explain this with an example.
Suppose you have a very simple OWL knowledge base where A is defined as anything which has at least a value for the property R, and B is defined as anything which has no value for the the property R - basically the only important thing is that the union of A and B are declared to cover the universe:

A = R some Thing
B = R max 0 Thing

Consider the following data:

:john :friend :mary
:john friend :andrea
:mary :loves :andrea
:andrea :loves :paul

:mary rdf:type A
:paul rdf:type B

or, graphically:

      :john
     /      \
    /:f      \:f
   v          v
:andrea <--- :mary  ---> A
   |     :l        :type
   |:l
   v
 :paul  ---> B
       :type

Consider the query:
{?X friend _:y, _:y rdf:type A, _:y loves _:z, _:z rdf:type B}

or, graphically:

?X
 |
 |:f
 v
_:y  ---> A
 |  :type
 |:l
 v
_:z  ---> B
    :type

If the bnodes in the query are interpreted as genuine existential variables, the answer should be: 
{{?X -> :john}}.
This is because there are two "alternative" completions of the data: one where (:andrea rdf:type A), and an alternative one where (:andrea rdf:type B).  This happens since A and B cover the universe, so for sure one of the two alternative completions has to be true. In both completions the evaluation of the query leads to {?X -> :john}, so this is the certain answer.

In the current spec the answer is empty, since bnodes can only bind to individuals or other bnodes, and in the data there is no binding that satisfies the query (since there is no unique "completion" of the data).

The moral is that the current spec does not capture correctly the expected existential meaning of bnodes for OWL direct semantics entailment, since the current spec just replicates for it the behaviour of bnodes in RDF, RDFS, OWL-RL (namely the binding only to bnodes or individuals - which is indeed correct in the scope of RDF, RDFS, and OWL-RL entailments).


So, my proposal would be - only in the case of the OWL Direct Semantics entailment regime - to allow (as an option -- say, with a flag -- or as an additional definition) for an extended meaning of bnodes in the query as proper existential nodes. In this case the answer to a query - when bnodes in the answer are filtered out - is monotonically richer (that is, any non-bnode element of the answer set in the original semantics is also in the answer set of this stronger semantics, but not viceversa). When treating bnodes as proper existential nodes in the case of the OWL Direct Semantics entailment regime, bnodes should be filtered out from the answer since nothing is known in the research literature about what happens when we leave them in (e.g., they may be infinitely many, since they are not restricted anymore to be bound to to existing nodes or blank nodes in the graph).

Let me know what do you think about this proposal.
I already had an informal chat about this with Birte, Axel, and Ivan, and they seem to be in favour if the majority agrees.

cheers
--e.

Enrico Franconi                  - franconi@inf.unibz.it
Free University of Bozen-Bolzano - http://www.inf.unibz.it/~franconi/
Faculty of Computer Science      - Phone: (+39) 0471-016-120
I-39100 Bozen-Bolzano BZ, Italy  - Fax:   (+39) 0471-016-009