Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

RE: RE: SUO: RE: First piece of 4D ontology




Dear Robert,

See comments below.

Regards  
      Matthew
============================================================
Matthew West - Principal Consultant
Operations & Asset Management, Shell Services International

Shell Visiting Professor
The Keyworth Institute, Leeds University

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/
============================================================ 

> -----Original Message-----
> From: Meersman Robert [mailto:meersman@vub.ac.be]
> Sent: 11 March 2001 19:14
> To: standard-upper-ontology@ieee.org
> Subject: re:RE: SUO: RE: First piece of 4D ontology
> 
> 
> 
> On Sun, 11 Mar 2001 18:41:50 +0100 West, Matthew MR 
> SSI-GREA-UK <Matthew.R.West@is.shell.com>  wrote:
> 
> >
> >Dear Robert,
> 
> ### Matthew, reply below--
> 
> --Robert Meersman
> 
> >
> >> ### Ian, Matthew,
> >> 
> >> ### am traveling in US so replies may be a bit slower. I had 
> >> also noticed the relationship between in Matthew's axioms #3 
> >> and #4 but in fact, why does the comment of #3 talk about 
> >> classes while the code is expressed using collection? Is that 
> >> accidental or intentional. 
> >
> >MW: Just an editiing accident. I'm having troubles picking 
> and using terms
> >consistently for the meanings I have.
> >
> >> Similarly, is "member of" the same 
> >> as "is a"?
> >
> >MW: Well I don't like to use "is a" because it can be 
> ambiguous in natural
> >language, being commonly used both for subclass-of and member-of.
> 
> ### The reason I asked is that you used it in the comments of 
> your axioms #1 and #3.

MW: I have tried to give 3 definitions for each axiom:

1. KIF
2. More or less direct translation of the KIF into English, retaining use of
variables.
3. following the i.e. an informal definition in everyday English. I have
only used "is a" in these last definitions. The meaning should be
interpreted from the more formal statements if you have any doubt. I expect
to use "is a" for "is a member of" and "is a type of" for "is a subclass of"
in the informal definitions.
> 
> >> 
> >> ### BTW these 4 axioms don't tell me a whole lot... not to 
> >> mention the serious agreement one needs about the "exists" 
> >> predicate and the implicit membership/is_a semantics. I 
> >> wonder how to use them. 
> >
> >MW: Please elaborate on the "serious agreement" that is needed.
> 
> ### You and others use KIF to specify axioms, rather than an 
> "accepted" syntax such as mathematics ("accepted" = "universally" 
> semantically agreed, at least since Hilbert and consorts --and 
> pardon the many quotes) in which, incidentally, the 4 axioms could 
> be written much more concisely. Clearly this is done with a certain 
> form of future computer processing in mind, i.e. interpretation by 
> a program for purposes of storage, validation, reasoning, ... by 
> computers. This requires a formal definition of the syntax used --in
> the case at hand this likely involves an (the!) ontology itself we 
> are trying to define. So, in order to avoid infinite regress, we 
> have no alternative but to axiomatically define (= agree on) the 
> basic predicates such as "exists ?x ?y". E.g. if this merely involves
> finite sets, one "only" has to agree on the definition of the 
> extension
> of ?x and on the lookup of ?y in this extension --but one 
> assumes there
> is more at play here, otherwise the whole SUO becomes an exercise 
> in triviality. I believe thick volumes of logic have been written on 
> this subject of "exists" alone (cfr. the Intuitionists, ...) so a
> proper initial agreement seems required. Of course I don't doubt that
> [the interpreter for] KIF++ has/will "prescribe" this; my point is 
> that it will be required at every step and needs to be performed 
> explicitly.

MW: Sounds like this question should be redirected to those who take 
responsibility for KIF.
> 
> ### Hope this helps for the time being. Apologies should replies 
> from me be even slower in the coming days, will be on the road
> 
> >
> >> Is there more to come?
> >
> >MW: Well the title does say "First piece", so I hope so, as 
> time permits.
> >> 
> >> --Robert Meersman
> >> 
> >> 
> >> >
> >> >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/
> >> >> ============================================================
> >> >> 
> >> >
> >> >
> >> 
> >> 
> >
> >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/
> >============================================================
> >
> >
> 
>