SUO: RE: Contrasting Starter Structural Ontology with R.Kent's formalisation
David,
. I am keen on getting means of visualising the ontologies,
since that vastly reduces the work involved in getting a feel for the
structure.
. Your mention of relationships makes me wonder whether what
you are proposing lends itself to some form of entity - relationship
modelling.
. Is there any relatively convenient visualisation of what you
are proposing, that we can view?
Thanks Graham Horn
Australian Institute of Health and Welfare
================================================
Phone: 02.6244.1094
Fax: 02.6244.1199
Email: Graham.Horn@aihw.gov.au <mailto:graham.horn@aihw.gov.au>
-----Original Message-----
From: David Whitten [mailto:whitten@lynx.eaze.net]
Sent: Friday, December 08, 2000 10:17 AM
To: standard-upper-ontology@ieee.org
Subject: SUO: Contrasting Starter Structural Ontology with R.Kent's
formalisation
>
>
> All,
>
> The sorted version of the theory of the Heraclitus distinction may be seen
> as a little clearer than the unsorted (one-sorted) version. Here there are
> three sorts of things: entities, individuals and classes. Let us denote
the
> sorts by $ent, $ind and $cls, respectively.
This is what I was doing in the structural ontology with Top,
Individual, and Class.
>
> SUO[$ent] denotes the ENTITY metaclass
> SUO[$ind] denotes the INDIVIDUAL metaclass
> SUO[$cls] denotes the CLASS metaclass
>
> So we do not need the corresponding 1-place metapredicate symbols.
But you introduced a non-KIF notation where I simply used INSTANCE-OF
> Sequent constraints on sorts are specified as follows.
>
> [necessity:] |- $ent
> [subtype:] $ind |- $ent and $cls |- $ent
> [disjointness:] $ind, $cls |-
> [covering:] $ent |- $ind, $cls
To do this in the Structural Ontology, I would introduce relations for
what you call necessity, disjointness, and covering. Since you are
reasoning at the meta-level, I would expect the axioms I would be
introducing would have to be interpreted in context of the statements
in the meta-language.
> This automatically induces the required partition
>
> SUO[*] = SUO[$ent] = SUO[$ind] + SUO[$cls]
>
> Finally, the sort of the INSTANCE-OF metapredicate symbol is specified as
> follows.
>
> sort[INSTANCE-OF] = <$ent, $cls>
>
different notation, but the same axioms, I think.
I said:
R050: (NTH-INSTANCE INSTANCE-OF 1 INDIVIDUAL)
R051: (NTH-INSTANCE INSTANCE-OF 2 CLASS)
R052: (NTH-ARGUMENT-NAME INSTANCE-OF 1 "?INS")
R053: (NTH-ARGUMENT-NAME INSTANCE-OF 2 "?TYPE")
R054: (VALENCE INSTANCE-OF 2)
R055: (INSTANCE-OF INSTANCE-OF RELATION)
> This automatically induces the required typing
>
> SUO[INSTANCE-OF] \subset SUO[$ent] x SUO[$cls]
>
> No axioms are necessary.
>
> Robert E. Kent
> rekent@ontologos.org
>
I could be wrong, but since you didn't state these in SUO-KIF, I'm
not convinced that "No axioms are necessary." but rather that
you chose to not state it in terms of axioms.
David (whitten@lynx.eaze.net) (713) 791-1414 ext 6116