From: <herman.ter.horst@philips.com>

Date: Tue, 24 Dec 2002 08:46:45 +0100

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-webont-wg@w3.org

Message-ID: <OFA2F5C8FE.D6F9B08A-ON41256C99.002A2EE2-C1256C99.002AEA8D@diamond.philips.com>

Date: Tue, 24 Dec 2002 08:46:45 +0100

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-webont-wg@w3.org

Message-ID: <OFA2F5C8FE.D6F9B08A-ON41256C99.002A2EE2-C1256C99.002AEA8D@diamond.philips.com>

> 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 > HermanReceived on Tuesday, 24 December 2002 02:48:55 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:56:49 UTC
*