Re: importing and entialment

Hi Pat,

You and I discussed this issue for a little while at the DAML PI
meeting, but I don't think we reached a resolution on it. So let me try
to explain it in writing. First let's assume a simple example for
discussion purposes:

Document A:
Man subclassOf Mortal

Document B:
B imports A
Socrates type Man

Now, if I understand you correctly, your proposal would say that if the
system failed to access document A (say by a 404 error), then document B
does not entail Socrates type Mortal. That is to say, any system that
did not conclude this could still be logically complete. However, I
would argue that this is undesirable, and that if you were unable to
load the statements from the imported file, then your answers would be
necessarily incomplete. To me this is no different from choosing to
ignore every other triple in a file. Any deductions you make are valid
(the system is sound), but you are clearly missing deductions that
logically follow (the system is incomplete).

Therefore, I ask what is the problem with defining imports in the terms
of entailment? If I understand correctly, the objection was that 404
errors then change the notion of entailement. I argue otherwise.
Entailment is a theoretical notion that does not depend on
implementation. Theoretically speaking the URIs used in imports
statements are just document identifiers, and documents are just
collections of statements. How you access a document is an
implementational issue, as is what happens when you get a 404 error. If
we say "A imports B means if B entails P then A entails P" then in terms
of entailment, it simply means if you can't access B (say due to a 404
error), then your reasoning is necessarily incomplete.

Just to be clear, let me try an analogy. Let's say we have a FOL theorem
prover that has decided for implementation reasons to store ground atoms
with different predicates in different files. Now it is possible that
one of these files might become corrupted. However, the system is robust
enough to continue reasoning with the rest of the information that it
has available. Does this require us to change our definition of FOL
entailment? Certainly not, we are talking implementation issues.
However, if one file was corrupted, we would argue that the system was
incomplete because there are entailments that it cannot deduce.
Therefore, OWL can still define imports using the notion of entailment
without being concerned about implmentation details such as 404 errors.


pat hayes wrote:
> The final discussion of owl:imports at the f2f kind of melted down,
> for which I take much of the blame. Afterwards it occurred to me how
> to phrase the statement everyone wanted to make about owl:imports so
> as to avoid all the unwanted implications. Not surprisingly, it is
> easy, and it has to do with the model theory:
> ------------
> owl:imports BBB
> is true in an interpretation I just when the owl KB gotten by
> dereferencing BBB is true in I, OR if there is no such owl KB.
> -------------
> If there isn't any such document, therefore, this is just plain true,
> which makes it kind of vacuous in that case. But if there is, then
> the imports assertion amounts to the same as asserting that KB inside
> this KB.
> So in this case:
> A:
> socrates rdf:type B:human .
> B:
> human rdfs:subClassOf mortal .
> C:
> owl:imports B
> socrates rdf:type B:human
> then A does not entail
> D: socrates rdf:type B:mortal
> but C does, provided of course that the imports worked; since in that
> case the imports statement is only true in interpretations which make
> B true. If the imports failed, then C wouldnt entail D, but not
> because 'entails' changes its meaning, but because in that case
> asserting C doesnt amount to saying as much as it does when the
> imports did work. In effect, C gets smaller when the imports fails.
> Note, this uses the usual notion of entailment, so entailment is not
> subject to the whims of 404 errors. Also note, this does not say that
> anyone is under any obligation to do anything (such as load a file) .
> It only says what is being claimed to be true.
> Pat
> --
> ---------------------------------------------------------------------
> IHMC                                    (850)434 8903   home
> 40 South Alcaniz St.                    (850)202 4416   office
> Pensacola                                       (850)202 4440   fax
> FL 32501                                        (850)291 0667    cell

Received on Monday, 21 October 2002 12:05:04 UTC