Re: Abstract Syntax and Semantics: review comments

From: herman.ter.horst@philips.com
Subject: Abstract Syntax and Semantics: review comments
Date: Fri, 20 Dec 2002 16:47:18 +0100

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

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

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.

> 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.
People are willing to try, of course, but I would much rather spend my time
in generating a proof procedure for OWL.

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

> - The document gives three definitions of OWL entailment (abstract, 
> DL en Full) but what is the normative definition of OWL entailment?. 

The document states that the direct model theory from section 2 is
authoritative for OWL/DL ontologies.  For OWL/Full ontologies, the
RDFS-compatible model theory is authoritative.

> The consensus summary said that in case of disagreement between 
> DL (fast) and Full (large) entailment, DL entailment is normative [2]. 
> In the new version, Peter introduced the
> words "authorative" (for the direct model theory) and "secondary" 
> (for the RDFS-compatible model theory) in the document. 
> I think the word normative should be used.

I can easily switch if this is the wording that should be used.

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

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

> Herman ter Horst 
> Philips Research 

peter

Received on Friday, 20 December 2002 12:36:04 UTC