Re: Abstract Syntax and Semantics: review comments

> Re: Abstract Syntax and Semantics: review comments
> From: Peter F. Patel-Schneider (pfps@research.bell-labs.com)
> 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, 
fast
> > and large) entailment coincide [2].  There is now an informative 
appendix
> > with a brief sketch in this direction.
> > I do not understand how the theorem given there follows from the 
lemma.
> > It does not seem to follow from the statement of the lemma alone: if I 
is 
> > an
> > OWL Full interpretation that satisfies K, then it needs to be proved 
that
> > 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 
lemma
> 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 
RDF
> 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., 
simple 
> > 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 
error.

It would be the responsibility of authors (and reviewers) to get it 
error-free,
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 
document
could be "lifted" to somewhat more abstract statements in the semantics 
document. 
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 
time
> 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 
automated
reasoning.

> 
> >  - 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 
triples.

...

> > - Section 2.1: A small simplification is possible: use the two rules 
for 
> > <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 
case
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 
counted
(in this description of the formal semantics of minCardinality, 
maxCardinality
and cardinality), and it is made clear that what you take the cardinality 
of is 
actually a set.

> 
> > Herman ter Horst 
> > Philips Research 
> 
> peter
> 

Herman