SUO: Re: Bootstrap Ontology
All, especially KIF experts,
The Boot Ontology needs a Cartesian product unary predicate
'(productRelation ?p1 ?p2)' for any two given unary predicates '?p1' and
'?p2'. What follows is a candidate definition of this. Please check to see
if this is correct.
__________
The Cartesian product unary predicate is define as follows.
(BinaryFunction productRelation)
(forall (?p1 ?p2 ?p)
(=> (= (productRelation ?p1 ?p2) ?p)
(and (UnaryRelation ?p1) (UnaryRelation ?p2) (UnaryRelation ?p))))
(forall (?p1 ?p2 ?i)
(<=> ((productRelation ?p1 ?p2) ?i)
(and (double ?i) (?p1 (first ?i)) (?p2 (last ?i)))))
The product projection functions are defined as follows.
(BinaryFunction projectionFunction1)
(forall (?p1 ?p2 ?f)
(=> (= (projectionFunction1 ?p1 ?p2) ?f)
(and (UnaryRelation ?p1) (UnaryRelation ?p2) (UnaryFunction ?f))))
(forall (?p1 ?p2 ?i ?i1)
(=> (= ((projectionFunction1 ?p1 ?p2) ?i) ?i1)
(and ((productRelation ?p1 ?p2) ?i) (?p1 ?i1))))
(forall (?p1 ?p2 ?i)
(= ((projectionFunction1 ?p1 ?p2) ?i) (first ?i)))
(BinaryFunction projectionFunction2)
(forall (?p1 ?p2 ?f)
(=> (= (projectionFunction2 ?p1 ?p2) ?f)
(and (UnaryRelation ?p1) (UnaryRelation ?p2) (UnaryFunction ?f))))
(forall (?p1 ?p2 ?i ?i2)
(=> (= ((projectionFunction2 ?p1 ?p2) ?i) ?i2)
(and ((productRelation ?p1 ?p2) ?i) (?p2 ?i2))))
(forall (?p1 ?p2 ?i)
(= ((projectionFunction2 ?p1 ?p2) ?i) (last ?i)))
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "Robert E. Kent" <rekent@ontologos.org>
To: "SUO" <standard-upper-ontology@ieee.org>
Sent: Saturday, January 20, 2001 10:40 AM
Subject: SUO: Bootstrap Ontology
>
> All,
>
> In the document [Appendix to Classification Metatheory] attached to the
> message [http://grouper.ieee.org/groups/ltsc/logs/ontology/msg00469.html]
> there is an type error in the socalled core axiom, which asserts "Relative
> instantiation-predication represented by '|=' is compatible with the
> absolute KIF instantiation-predication.", and is formalized by the KIF
> sentence
>
> (forall (?c ?i ?t)
> (and (=> (|= ?c ?i ?t) (?t ?i))
> (=> (not (|= ?c ?i ?t)) (not (?t ?i)))))
>
> In the relative instantiation-predication notation
>
> (|= ?c ?i ?t)
>
> the variables '?c', '?i' and '?t' have the types 'Classification',
> 'Instance' and 'Type', respectively.
>
> However, in the universal (absolute), and basic KIF,
> instantiation-predication notation
>
> (?t ?i)
>
> the variables '?t' and '?i' should have the types 'UnaryRelation' and
> 'Object', respectively, where the latter denotes the universal type of all
> KIF objects.
> __________
>
> So two things need to be done here.
>
> First, we need to define a *Bootstrap Ontology*, which will mesh the needs
> of the Classification Ontology (and other Information Flow metatheories in
> the future) with KIF. Note that this Bootstrap Ontology is NOT the
> Structural Ontology, which is being replaced and augmented by a collection
> of metatheories that allow one to build ontologies in a principled fashion
> from basic ontologies with constructor operations.
>
> Second, we need to correct the core axiom error mentioned above.
> __________
>
> The Bootstrap Ontology needs (at least for now) the following categories
of
> things:
>
> Object -- the universal type
> Relation -- the sum of all relation types
> UnaryRelation
> BinaryRelation
> TernaryRelation
> Function -- the sum of all function types
> UnaryFunction
> BinaryFunction
>
> I will assume the following partitions:
>
> Object = Relation + Function + ...
> Relation = UnaryRelation + BinaryRelation + TernaryRelation + ...
> Function = UnaryFunction + BinaryFunction + ...
> __________
>
> The core axiom error is fixed as follows.
>
> Define a binary KIF function 'int' that denotes the intent of an instance
> 'i' in a classification 'c' defined by
> int(i) = {t in typ(c) | i |= t}.
>
> (BinaryFunction int)
> (forall (?c ?i ?p)
> (=> (= (int ?c ?i) ?p)
> (and (Classification ?c) (inst ?c ?i) (UnaryRelation ?p))))
> (forall (?c ?i ?t)
> (=> (and (Classification ?c) (Instance ?i) (Type ?t))
> (<=> (int(?c ?i) ?t) (|= ?c ?i ?t))))
>
> Dually, define a binary KIF function 'ext' that denotes the extent of a
type
> 't' in a classification 'c' defined by
> ext(t) = {i in inst(c) | i |= t}.
>
> (BinaryFunction ext) ;; we need to change to name of the extensibility
> predicate
> (forall (?c ?i ?p)
> (=> (= (ext ?c ?t) ?p)
> (and (Classification ?c) (typ ?c ?t) (UnaryRelation ?p))))
> (forall (?c ?i ?t)
> (=> (and (Classification ?c) (Instance ?i) (Type ?t))
> (<=> (ext(?c ?t) ?i) (|= ?c ?i ?t))))
>
> Finally, using the KIF predicate 'ext', the core axiom now becomes the KIF
> sentence
>
> (forall (?c ?i ?t)
> (and (=> (|= ?c ?i ?t) (ext(?c ?t) ?i))
> (=> (not (|= ?c ?i ?t)) (not (ext(?c ?t) ?i)))))
>
> But this is redundant by the third axiom above for the KIF predicate
'ext'.
> So toss it out.
>
> Robert E. Kent
> rekent@ontologos.org
>