RE: [FULL] ISSUE-119: the other approach

Ian Horrocks wrote on Monday, May 19, 2008:

>I talked to Peter about this and we agreed that Jeremy's proposal
>looks promising.
>
>I would like to hear from Michael as to what he thinks about this
>proposal.
>
>Ian

I went in this direction myself a few weeks ago, but then I found that
Jeremy has already been there a few /years/ ago. :-)

Yes, I agree with Jeremy's approach in general, though I might have a
slightly different view on it. I do not see this approach so much as an
"other approach", but rather as a variation of the idea of comprehension
principles. I will explain this in more detail below. 

In addition, I have some difficulties with convincing myself that Jeremy's
suggested adaptation of Theorem 2 will work in all possible cases (provided
that I correctly understand his suggestion). I will propose an alternative
modification of Theorem 2, which IMO is still in line with Jeremy's
approach, and for which it seems to be easy to show a certain strong
relationship with the original Theorem 2. 

The basic idea of Jeremy's approach is to put those parts of the RHS of a
DL-entailment, which are produced by comprehension principles, to the LHS of
the investigated entailment. I will call these entailments, which follow
from both the given ontology *and* the comprehension principles, as
"CP-entailments" -- i.e. an entailment, which follows alone from the
ontology, even if there wouldn't be comprehension principles, is /not/ a
CP-entailment. 

Having some of the CP-entailments on the LHS of an entailment may look like
a trick. But what the comprehension principles do is technically not
different from just adding the full collection of these CP-entailments to
the premise (the LHS!) of an investigated entailment /automatically/. So, if
either the full collection of CP-entailments exists in the entailment
closure of an investigated entailment's LHS, or if it is explicitly added to
that LHS, both approaches will lead to exactly the same results.

Here, I want to say what my concern is with Jeremy's modification of Theorem
2. I understand Jeremy's suggestion (@Jeremy: please correct me!) in the way
that one looks at the RHS of the investigated DL-entailment, and checks for
all sub graphs of the RHS whether they have the form of a graph produced by
the comprehension principles. However, I suspect that the following
situation may occur: A certain DL entailment is also an entailment in Full
/with/ comprehension principles, but not an entailment in Full with/out/
comprehension principles, and there is not a single sub graph at the RHS of
the entailment which has the form of a product of the comprehension
principles. My point is that I suspect it to be possible that the "direct"
conclusions of the comprehension principles may entail further conclusions,
which do not have the form of a comprehension principle product. In this
case, one would not be able to recognize those parts of the RHS, which have
to be added to the LHS.

The following alternative modification of Theorem 2 does not have this
problem, since it talks about /all/ CP-entailments of an ontology O, i.e.
/every/ entailment of O, which only exists due to the existence of the
comprehension principles. This includes such entailments which do not have
the form of a comprehension principle product. Further, my proposal does not
take the RHS of the investigated entailment into account at all. So the
triples added to the LHS do not necessarily have to match parts of the RHS
in any way.

This is my proposed modification of Theorem 2:

    "If A and B are valid OWL DL ontologies,
    and RDF(A) and RDF(B) are their RDF mappings,
    and A DL-entails B,
    then there /exists/ some subset S of all CP-entailments of RDF(A)
    such that S + RDF(A) Full-entails RDF(B)."

This formulation is actually equivalent to Theorem 2 together with
comprehension principles (see below for a proof). This means that there
would even be zero additional effort on the WG side: For OWL 1 Full, Peter's
proof of Theorem 2 is also a proof for the modified version above. And in
OWL 2 Full, it will suffice to extend Peter's proof to the new constructs,
by applying the same techniques as before. This would have to be done again,
anyway (and, of course, I would appreciate if Peter would be the one who
does it again :-)). 

While the proof for OWL 2 Full would take the comprehension principles into
account (as in OWL 1), they wouldn't be needed anymore as part of the logic.
The advantage of the modified theorem is that it allows to only take such
CP-entailments into account, which are actually needed to make the
investigated DL-entailment visible in OWL Full, too. This is because of the
existential quantifier in the modified theorem. In particular, the
formulation allows to always assume, without loss of generality, that the
set of added triples is /minimal/ w.r.t. the "Theorem-2-property". This
might, perhaps, become relevant for a future consistency proof for OWL 2
Full.
 
The not-so-nice aspect of the formulation above is that it doesn't give
implementers a hint how to choose such a subset, it just talks about the
/existence/ of such a subset. However, I regard it to be the OWL-WG's
primary goal to make sure that there is a close semantic relationship
between DL and Full, and the relationship for OWL 2 should in the best case
mirror the one of OWL 1. For this purpose, the above theorem seems perfectly
sufficient. Certainly, a more "constructive" formulation would be nice and
useful, but I think it is out of scope for this WG to put additional energy
on this kind of research.

Best regards,
Michael

PS: Proof for the equivalence of {Theorem 2 + comprehension principles} and
{modified Theorem 2 without comprehension principles}:

Let A and B be valid OWL DL ontologies, and let RDF(A) and RDF(B) be their
RDF-mappings.

Let S*(A) be the complete set of CP-entailments for RDF(A), i.e. the set of
RDF triples defined by: 

  { Entailment closure of RDF(A) w.r.t. OWL Full /with/ comprehension
principles }
  minus
  { Entailment closure of RDF(A) w.r.t. OWL Full /without/ comprehension
principles }

or written in a shorter form:

  (1): S*(A) = Entailments_Full+Compr( RDF(A) ) - Entailments_Full\Compr(
RDF(A) )  

where "Full+Compr" means "OWL Full /with/ comprehension principles, and
"Full\Compr" means OWL Full with/out/ comprehension principles.

(1) can be restated as:

  (2): Entailments_Full+Compr( RDF(A) ) = S*(A) + Entailments_Full\Compr(
RDF(A) )

Now the entailment

  (3): RDF(A) Full+Compr-entails RDF(B)

holds if and only if

  (4): Entailment (3) is a member of Entailments_Full+Compr( RDF(A) )

which, according to (2), is true if and only if

  (5): Entailment (3) is a member of S*(A) + Entailments_Full\Compr( RDF(A)
)

which is the same as saying:

  (6) S*(A) + RDF(A) Full\Compr-entails RDF(B)

This, again, is equivalent to:

  (7) There exists some subset S of S*(A) with 
      S + RDF(A) Full\Compr-entails RDF(B)

Direction "(6)==>(7)" is trivial, since S*(A) itself is such a subset of
S*(A). 

Direction "(6)<==(7)" follows from "S+RDF(A) subset S*(A)+RDF(A)", together
with monotony of OWL-Full entailment.

So from (3) and (7) we get:

    RDF(A) Full+Compr-entails RDF(B)
  if and only if
    There exists some subset S of S*(A) with 
    S + RDF(A) Full\Compr-entails RDF(B)

Hence:

    (Theorem 2)
    A DL-entails B ==> RDF(A) Full+Compr-entails RDF(B)
  if and only if
    (Modified Theorem 2)
    A DL-entails B ==> There exists some subset S of S*(A) with 
                       S + RDF(A) Full\Compr-entails RDF(B)

.

>On 28 Apr 2008, at 16:55, Jeremy Carroll wrote:
>
>>
>> We have discussed a different approach to comprehension, which was
>> perhaps poorly branded as 'solipistic' ....
>>
>> Peter and others have described this as a big change; the point of
>> this message is to argue to the contrary that it is small - both in
>> the amount of text of the spec that changes, and in the amount of
>> code that changes as a result. In fact, I suggest that 0-lines of
>> code change. Hence, this would be a backward compatible change.
>>
>> =====
>>
>>
>> Current state OWL1:
>>
>>
>> + Comprehension principles + Theorem 2
>>
>> These give a weak alignment of DL entailment and Full entailment
>>
>> Full reasoners (such as Jena Rules) partially implement this, by in
>> some circumstances introducing terms that match the constructs in
>> the comprehension principles.
>>
>>
>> Possible alternative:
>>
>> Comprehension principles remain, not as model theoretic principles,
>> but as reasoning principles.
>>
>> Theorem 2 is modified from approx:
>>
>> If A DL-entails B where A and B are in the syntactic subset then
>>    A Full-entails B.
>>
>> To approx.
>>
>> If  A DL-entails B  where
>>     A and B are in the syntactic subset
>> then
>>     B = B' & B''
>> where B'' is a conjunct of terms matching comprehension principles
>> and
>>    A & B'' Full-entails B
>>
>>
>> =====
>>
>> This modifies the comprehension principles from being model-
>> theoretic statements, to play a role in theorem 2 that speaks more
>> to the proof-theory. Since OWL Full implementations implement rules
>> (i.e. proofs) this proof-theoretic variant of comprehension is
>> closer to what the implementations already do, and there is no
>> backward compatibility problem. (Backward compatibility is about
>> OWL implementations and OWL documents, not about OWL specifications).
>>
>> Also, the textual change to the spec is slight - the comprehension
>> principles remain - but their role in the OWL Full semantics is
>> modified.
>>
>>
>> Jeremy
>>
>>
>>
>>
>>