W3C home > Mailing lists > Public > www-rdf-logic@w3.org > November 2000

Re: A Model Theoretic Semantics for DAML-ONT

From: Richard Fikes <fikes@KSL.Stanford.EDU>
Date: Tue, 14 Nov 2000 15:42:16 -0800
Message-ID: <3A11CDD8.EA4A67F6@ksl.stanford.edu>
To: Dan Connolly <connolly@w3.org>
CC: Deborah McGuinness <dlm@KSL.Stanford.EDU>, www-rdf-logic@w3.org
Thanks much for your comments.  Here are some detailed replies from me.

> * title is misleading; suggestion:
>         An axiomatic specification of DAML-ONT


> * clarification: this seems to imply (Thing 1)
> and (Thing "abc") and (Thing ^(1 2 3)),
> i.e. that everything in the KIF
> universe of discourse (integers, strings, lists etc.)
> is a daml:Thing:
> | %% Every object is an instance of Thing.
> | (Thing ?x)
> If that's what you had in mind, please be explicit.
> I think it's also what I had in mind, but it
> seems quite different from the OIL semantics.

Yes, that is what we had in mind.  We thought we had been explicit with
the comment: "Every object is an instance of Thing.".

> * How do we avoid Russel's paradox.
> It seems easy enough to run into; just define A
> ala:
>         (<=> (A ?x) (not (holds ?x ?x))
> then, assuming (holds P X) can be used
> interchangeably with (P X), we have:
> (A A)       => (not (holds A A)) => (not (A A)) !
> (not (A A)) => (not (holds A A)) => (A A) !
> Is there some restriction which avoids
> the above definition of A?

No.  There is nothing in a first order language such as KIF that
prevents one from creating logically inconsistent logical theories.  I
don't see that the axioms that we have written for DAML-ONT make that
situation any better or worse.

I am not an expert on paradoxes.  Pat Hayes would be the person to ask
further questions about paradoxes.

> * This looks like overspecification:
> | %% Classes that are disjointWith have no instances in common,
> | and at least one of the classes has an instance.
> where do you get the last bit? Surely it's the case that
> (disjointWith Nothing Nothing), no?

The restriction that at least one of the classes has an instance was
indeed one that we thought was intended but that was not explicitly
mentioned in the spec.  So, consider that restriction to be a proposed
axiom.  Our intuition was that we did not want Nothing to be disjoint
with itself.

> * Umm...
> | %% The second argument of ?cardinality? is a non-negative integer.
> actually, the second argument of cardinality is a string
> that denotes a non-negative integer, I'm afraid.

Oh.  I assumed that numbers were in the domain of discourse, as they are
in KIF.  So, do we need to define something like a "numerical string"
that is a string consisting of digits and an optional decimal point?

> * Yikes!
> | Note that this formulation assumes a finite number of second
> | arguments for a given property and first argument.
> That seems like a hasty limitation!

I don't think it is a problem, because this formulation is only used in
specifying cardinality restrictions, which need not include infinity.

> * This follows the bogus interpretation of rdfs:domain:
> | %% The first argument of onProperty is a restriction or a
> | qualification.
> | (=> (onProperty ?rq ?p) (or (Restriction ?rq) (Qualification ?rq)))
> Following your own specification for domain below, this should be:
>  (=> (onProperty ?rq ?p) (Restriction ?rq) )
>  (=> (onProperty ?rq ?p) (Qualification ?rq) )
> i.e.
>  (=> (onProperty ?rq ?p) (and (Restriction ?rq) (Qualification ?rq) ) )

I think this problem is fixed in the new version sent out last evening.

> in fact, Restriction and Qualification might be different
> names for the same class; I hope to get rid of one of them.

Seems right to me.

> * This is perhaps overspecification:
> | %% Both arguments of ?imports? are ontologies.
> In general, any document can import another document.
> But there's nothing to say that the class of ontologies
> is any smaller than the class of documents, so perhaps
> it doesn't matter.

Oh, I thought that both argument to "imports" had to be ontologies.  If
that is not the case, we can remove that axiom.

Thanks again for your comments.

Received on Tuesday, 14 November 2000 18:42:04 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:45:35 UTC