Re: Abstract Syntax and Semantics: review comments

> Re: Abstract Syntax and Semantics: review comments
> From: Peter F. Patel-Schneider (
> Date: Fri, Dec 20 2002 

> > Abstract Syntax and Semantics: 
> > review comments about version of 19 December
> [...]
> > - Correspondence between OWL DL entailment and OWL Full entailment.
> > The Bristol consensus on semantics already expressed the need for a 
> > characterization of the situation that DL and Full (in those days, 
> > and large) entailment coincide [2].  There is now an informative 
> > with a brief sketch in this direction.
> > I do not understand how the theorem given there follows from the 
> > It does not seem to follow from the statement of the lemma alone: if I 
> > an
> > OWL Full interpretation that satisfies K, then it needs to be proved 
> > I satisfies C.  Getting another OWL DL interpretation I' that 
> > satisfies K, shows that I' satisfies C.  And then?
> > 
> > Until we can really view the lemma and the theorem and its converse 
> > as proved, we do not really know about the correspondence between 
> > OWL DL entailment and OWL Full entailment.
> The theorem follows from the proof of the lemma, namely that the mapping
> between OWL-interpretations and OWL/DL-interpretations is uniform for a
> given separated vocabulary.  I will strengthen the statement of the 
> accordingly.

> > - The entailment definitions in the document are theoretical, 
> > in terms of models.
> This is as it should be.

I do not question this.

> > It would be useful to have more practically useful, triple-based 
> > characterizations of entailment, as in the RDF Semantics document [3].

For clarity: I would like to add such characterizations to the basic,
theoretical definitions.

> The closure characterizations in the RDF semantic document are 
> non-normative and prone to bugs.  If this is true for RDF, which is very
> simple, think how difficult it would be to define the OWL-closure of an 
> graph.

I can see that it is difficult, therefore the next suggestion.

> > As long as such characterizations remain unknown, 
> > a sequence of simple sufficient conditions for entailment (i.e., 
> > inference rules, formally stated, with proofs of validity) could 
> > form a useful informative addition to the document in order to 
> > familiarize people with the various kinds of OWL entailment. 
> Again, the generation of such rules is very difficult and prone to 

It would be the responsibility of authors (and reviewers) to get it 
after which users would have the benefit.
I am thinking of simpler rules, for example like the ones used implicitly
in the short example appendix to the OWL Semantics document.
Or: several rules for entailment (or non-entailment) appearing in the test 
could be "lifted" to somewhat more abstract statements in the semantics 
Such rules would not need to form a complete set.
They could help to bridge the gap between the basic theoretical 
definitions of 
entailment and practical situations.

> People are willing to try, of course, but I would much rather spend my 
> in generating a proof procedure for OWL.

A proof procedure is relevant, of course.
A (sound and complete) proof procedure for OWL, based on OWL in the form 
of RDF 
triples, would give a special kind of triple-based characterization of 
OWL entailment that I mentioned above, one that could be used for 

> >  - It would also be nice to know how an OWL DL KB is characterized in 
> > triple form.  That is, what is an "OWL DL graph" as a special kind of 
> > RDF graph?
> This is the subject of section 4 of the document.

Section 4 defines "OWL DL graphs" (without naming them in this way)
as the outcome of a translation process from abstract syntax to RDF.
Since RDF graphs are the exchange syntax, it would be interesting to also 
have an 
alternative definition of such OWL DL graphs purely in terms of RDF 


> > - Section 2.1: A small simplification is possible: use the two rules 
> > <annotation> also in <directive>, instead of their content. 
> The rules are somewhat different, so reuse is not easily possible.

The only difference that I see is that the word "annotation" starts in one 
with a capital and in the other case with a small letter.

> > - 5.2: In the tables defining the cardinality restrictions: 
> > instead of card({v:<u,v>...) make it completely explicit with the set 
> > from which v can be taken:  card({v elementOf ...:<u,v>...) 
> This is not needed as card({v:<u,v> in EXT(...)}) delimits the set
> appropriately.

I understand what you mean, by means of information that I can guess from 
the document.  There is a small, formal point, however.
I propose three very simple additions to the table in the following way:
{v elementOf IOT : <u,v> in ...} instead of {v: <u,v>...}.
In this way it is made completely explicit which elements are to be 
(in this description of the formal semantics of minCardinality, 
and cardinality), and it is made clear that what you take the cardinality 
of is 
actually a set.

> > Herman ter Horst 
> > Philips Research 
> peter


Received on Tuesday, 24 December 2002 02:48:55 UTC