From: Richard Fikes <fikes@KSL.Stanford.EDU>

Date: Thu, 16 Nov 2000 17:34:27 -0800

Message-ID: <3A148B23.FA80EE59@ksl.stanford.edu>

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

CC: www-rdf-logic@w3.org

Date: Thu, 16 Nov 2000 17:34:27 -0800

Message-ID: <3A148B23.FA80EE59@ksl.stanford.edu>

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

CC: www-rdf-logic@w3.org

Here are some hopefully helpful comments on your new version of the model-theoretic semantics for DAML-ONT and your introductory comments to that version. > The > transliteration from words to symbols from set theory introduces no use of > anything like ``holds'' or ``type'' into the semantics. As I said before, the axiomatization document does not introduce "type" into the semantics. "type" is a property in DAML-ONT and axioms are included in the document to describe its meaning. > The set theory is naive set theory, which is > all that is needed, as there is no set of sets, etc., required. Well, that isn't clear. Since "Class" and "Property" are defined in DAML-ONT to be classes, it seems that specific classes and properties are considered to be in the domain of discourse and therefore that one can have classes of classes and classes of properties. So, a set theoretic semantics would seem to require a provision for sets of sets. > The > semantics covers almost all of DAML-ONT, missing only lists. I don't see > how lists contribute to the semantics of DAML-ONT in any case. (If someone > can say how they contribute, please let me know.) If any other portion of > the semantics of DAML-ONT is missing, please let me know. Missing seem to be all of the axioms that say whether a given term (e.g., Thing, Literal, cardinality) is a property or a class, and the axioms that define or restrict the possible interpretations of List, Empty, asClass, first, rest, and item. > I think that the semantics is thus as formal as would be required. We seem to have a basic disagreement here. A primary purpose of the axiomatization that Deborah and I wrote is to provide a *formal* and *precise* description of the intended meaning of the constructs in the DAMl-ONT language. The community already has English prose descriptions of the intended meaning of DAML-ONT, RDF, and RDF SCHEMA. What is missing are formalizations of that prose. Much of your semantics document consists of informal English prose descriptions of axioms that are in the axiomatization document. For example, the model-theoretic semantics document says: If <type,[?X1,...,?Xn],Disjoint> is in KB then IC(?Xi) and IC(?Xj) are disjoint for i different from j. Correspondingly, the axiomatization document says: %% Saying that an object is "Disjoint" is equivalent to saying that the object is a list, that every item in the list is a class, and that the classes in the list are pairwise joint. Ax8. (<=> (Disjoint ?l) (and (List ?l) (forall (?c) (=> (Item ?c ?l) (Class ?c))) (forall (?c1 ?c2) (=> (Item ?c1 ?l) (Item ?c2 ?l) (/= ?c1 ?c2) (DisjointWith ?c1 ?c2))))) It seems to me that we need the formal expression of the statements that are in the current version of the model-theoretic semantics document, and that most of that formalization will look very much like what is in the axiomatic semantics document. The primary difference at this point seems to be your use of set theory (i.e., considering a class to be a set) and our use of relations (i.e., considering a class to be a unary relation) to state the same meanings. As is always the case, creating the formal statements leads to a more precise description. For example, many of the axioms in the axiomatization are bi-directional (i.e., if-and-only-if) sentences, whereas the corresponding statements in the model-theoretic semantics document are only unidirectional. Also, domain and range implications (e.g., "(=> (Disjoint ?l) (List ?l))") seem to be missing in most of the statements in the model-theoretic semantics document. So, I would urge us as a community to produce *formal* descriptions of the semantics of DAML-ONT, irrespective of what formalism is used to express the description. RichardReceived on Thursday, 16 November 2000 20:34:14 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:32 UTC
*