SUO: RE: RE: First piece of 4D ontology
Dear Ian,
> > Dear Colleagues,
> >
> > Please find below a first piece of a 4D ontology.
> >
> > I'd like to thank Pat Hayes for reviewing some early drafts.
> >
> > Comment text is of two types:
> > 1. Translations into English of the KIF below. I assume that
> > eventually automatic translation from KIF into e.g. ACE
> > will be possible for human interaction.
> > 2. Structuring information, e.g. Subject Area, Theory, Statement No.
> > These are things that I think we need to support engineering
> > an ontology (vs. saying what we mean) which I hope will be
> > supported by KIF before long.
> >
> > Comments are welcomed.
> >
> > ; Subject Area: Thing
> > ;
> > ; theory: individual and collection
> > ; uses:
> > ;
> > ; #1:
> > ;
> > ; For all X, X is a thing.
> > ;
> > ; i.e. that which everything is a member of.
> > ;
> > ; Note 1: In First Order Logic there is no need to make any
> > declaration,
> > ; (forall ?x ...) is sufficient.
> > ; Note 2: This means that all collections will be a
> subclass of thing.
>
> This axiom also appears in the merged ontology. There it has
> the following
> form: (forall (?X) (instance-of ?X Entity))
MW: Yes. Note however, that this axiom is commented out here since it is
unnecessary in a language with lambda calculus.
>
> > ;
> > ; #2:
> > ;
> > ; for all X, if there exists a Y and Y is a member of X,
> then X is a
> > ; member of collection.
> > ;
> > ; i.e. any thing that has a member is a collection.
> > ;
> > (forall ?x
> > (=> (exists ?y
> > (?x ?y)
> > )
> > (collection ?x)
> > )
> > )
> > ; Note: This (?x ?y) is not valid SUO-KIF today, but I
> understand it
> > ; will be in the near future.
>
> You could express (?x ?y) as (instance-of ?y ?x), which is
> syntactically
> well-formed SUO-KIF. However, it is also not a first-order
> sentence.
MW: Yes, but I don't think instance-of is as good style. It introduces a
second way of saying "is member of" which then begs the question of what
is the difference between them.
>
> I'm wondering what you mean by "collection" in your axiom. I
> thought we
> were using this term to denote things like wolf packs,
> football teams, etc.,
> which are set-like, in that they have members, but, unlike
> sets, they have a
> spatio-temporal location. However, if this is what you mean, then you
> exclude sets and classes, which have members but are not
> collections in the
> sense just explained.
MW: In this context the string "collection" is a label that means precisely
what the axioms say it means, not more and not less. So do sets and classes
meet the axioms as stated? I.e. do they have members? If so then they are
also collections.
>
> > ;
> > ; #3:
> > ;
> > ; For all X, X is an individual, or X is a class.
> > ;
> > ; i.e. everything is either an individual or a class
> > ;
> > (forall ?x
> > (or (individual ?x)
> > (collection ?x)
> > )
> > )
>
> Note that axiom #3 is redundant, since it is logically
> entailed by axiom #4.
MW: You are right. I misread #4 (I'm still very much learning how to write
KIF and learning to understand what it really means).
>
> > ;
> > ; #4:
> > ;
> > ; For all X, if X is a member of collection then X is not a
> > ; member of individual and vice versa.
> > ;
> > ; i.e. any thing that is not a collection is an individual, and
> > ; vice-versa.
> > ;
> > (forall ?x
> > (<=> (collection ?x)
> > (not (individual ?x))
> > )
> > )
>
> My earlier comment about "collection" applies here as well,
> since this axiom
> appears to rule out sets and classes.
MW: How so?
>
> > ;
> > ; end theory
> > ;
> > ; end subject area
Regards
Matthew
============================================================
Matthew West
Operations & Asset Management - Shell Services International
Shell Visiting Professor, The Keyworth Institute
H3229, Shell Centre, London, SE1 7NA, UK.
Tel: +44 207 934 4490 Fax: 7929 Mobile: +44 7796 336538
http://www.shellservices.com/
http://www.keyworth.leeds.ac.uk/
http://www.matthew-west.org.uk/
============================================================
application/ms-tnef