SUO: Re: Contrasting Starter Structural Ontology with R.Kent's formalisation
David,
I am starting to develop a structural framework at the metalevel in both
regular unsorted KIF and in comparison, my idea of a sorted version of KIF
following Enderton, but adding on sort constraints for expressibility. But I
am also giving a formal semantics (interpretation) for this metalanguage.
This will be somewhat comparable to your started structural ontology, but
with a different point of view. More to come.
By "no axioms necessay" I meant no metaleval axioms needed to be expressed
as KIF sentences. There are axioms, but they are encoded as sort constraints
and sort typings.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "David Whitten" <whitten@lynx.eaze.net>
To: <standard-upper-ontology@ieee.org>
Sent: Thursday, December 07, 2000 3:17 PM
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