Re: model-theoretic semantics for DAML-ONT

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.

Richard

Received on Thursday, 16 November 2000 20:34:14 UTC