SUO: RE: First piece of 4D ontology
Matthew,
Please see my comments below.
-Ian
> -----Original Message-----
> From: West, Matthew MR SSI-GREA-UK
> [mailto:Matthew.R.West@is.shell.com]
> Sent: Thursday, March 08, 2001 1:22 AM
> To: Standard-Upper-Ontology (E-mail)
> Subject: First piece of 4D ontology
>
>
> 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))
> ;
> ; #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.
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.
> ;
> ; #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.
> ;
> ; #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.
> ;
> ; 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/
> ============================================================
>