Re: datatyping in test for Pat's review

On May 26, Jeremy Carroll writes:
> 
> Ian suggests:
> [[
> An OWL DL document D is consistent with respect to datatype theory T if
> and only if there is some Abstract OWL interpretation I with respect
> to T such that I satisfies D.
> ]]
> 
> unfortunately this text, while neat, asks more questions than it answers - we 
> do not define satisifes as in an interpretation satisfying a document, so 
> questions to do with 
> a) imports closure 
> b) which abstract ontology
> are unanswered.

The definition of satisfies can be found in S&AS Section 3.4. It talks
about ontologies rather than documents, but I thought that when we
discussed this in Budapest you said that you would say something like
"satisfies and ontology O that is equivalent to D". The semantics of
an ontology takes import closure into account, so that comes for
free.


> 
> My proposed text:
> 
> [[
> An OWL Lite or OWL DL document is consistent with respect to a datatype theory 
> [OWL Semantics and Abstract Syntax], if and only if a corresponding 
> collection of OWL DL ontologies in abstract syntax form with a separated 
> vocabulary is simulataneously consistent with respect to the datatype theory.
> ]]

I think that this is worse as you introduce a new term
"simultaneously consistent" that is not defined and whose meaning
isn't completely clear. (I imagine that what you mean is that there is
some interpretation that satisfies all of the ontologies.) I don't
believe you need to talk about a collection (because the semantics
takes imports closure into account) or separation (because this is
part of the definition of an interpretation), so it is enough (and
much clearer) to say:

[[ 
An OWL Lite or OWL DL document is consistent with respect to
datatype theory [OWL Semantics and Abstract Syntax] if and only if a
corresponding OWL DL ontology in abstract syntax form is consistent
with respect to the datatype theory [OWL Semantics and Abstract
Syntax].
]]

Ian


> 
> requires the somewhat shorter imaginitive leap from the defn of consistent in 
> S&AS to the notion of simulataneously consistent, and perhaps is still 
> unclear about imports. However, the which abstract ontology is answered by 
> the "with a separated vocabulary" and the correspondence theorem.
> 
> I will circulate some more text tomorrow.
> 
> Jeremy
> 
> 
> 
> 
> 
>

Received on Monday, 26 May 2003 16:31:58 UTC