ontolingua theory inclusion

Tom Gruber <Gruber@KSL.Stanford.Edu>
Full-Name: Tom Gruber
Message-id: <2955142277-1298535@KSL-Mac-69>
Date: Mon, 23 Aug 93  17:51:17 PDT
From: Tom Gruber <Gruber@KSL.Stanford.Edu>
To: ontolingua@KSL.Stanford.Edu
Subject: ontolingua theory inclusion 
Here's a FAQ about ontolingua's theory inclusion.

> I have a couple of questions regarding ontologies ("The Role of Common
> Ontology in Achieving Sharable, Reusable Knowledge Bases", yourself,
> Jan 91).

> Is it possible to have ontologies as "specialisations" on other
> ontologies ?  That is, can taxonomic lattices (ala KL-ONE, LOOM) of
> ontologies be established ?  Consider the following example where O is
> some ontology and a,b,c and d are some arbitrary numbers (say
> integers) such that a<b<c<d :

>               an ontology O exists which defines the range for some
>               attribute A (or, i suppose function in ontolingua-speak) of a..d.
>               That is, A lies in the range of a and d.

>               an application APP1 adopts O but only uses A over the range
>               a..b and operates under this assumption i.e.  it will break if
>               something outside of a..b is encountered.

>               another application APP2 adopts O but only uses A over the
>               range c..d and will experience the same heartburn if something
>               outside of c..d pops up.

> Both APP1 and APP2 adopted the ontology O in the hope of being able to
> exchange information.  The range of A in O (a..d) encompasses both a..b
> and c..d and so is the least generalisation of the two and would be
> adopted.  If, however there had been ontologies O2 and O3 that were
> both specialisations of O with respect to A, then APP1 and APP2 could
> safely interoperate over those parts inherited from O but not
> specifically overridden and hence incompatible in APP1 and APP2.

> Hence, there seems to be some scope for taxonomic lattices of
> ontologies.  Something seems a little wrong in this argument, though,
> as ontologies are not referred to in your papers as things which are to
> be, as it were, created "liberally" (unlike concepts in the TKRs that i
> speak of - loom, etc).  I can't put my finger on the problem in this,
> though.

Yes, it is possible to partition ontologies for this purpose.
Ontolingua supports the notion of a theory.  A theory is given by a
set of axioms.  So ontology/theory O could have "child" theories O2
and O2 that only add the additional restrictions on A that you talked
about.  Theories O2 and O3 would "include" theory O, meaning that the
axioms of O are unioned with the axioms in O2 to specify the theory
O2.  We used this feature extensively in the engineering math
ontologies and configuration design ontology.  For example, here is
the definition of a component in the more general ontology,
configuration-design:

(define-class COMPONENT (?x)
  "A component is a primitive module or assembly of primitive modules
that participate in a design.  Components need not correspond to
physically whole objects such as standard parts from a parts catalog.
Components may also represent functional and behavioral abstractions.
This ontology only says that components are the locus of attributes
and constraints.  To say that a component C has-attribute A means
that there is a function A from C to the value of the attribute.
In object-oriented terminology, one can think of A as a slot of C, 
and calling it an attribute means that it may be mentioned
in constraints on C.  Similarly, a component C has-subpart S means 
the function S maps C to another component which plays the S role
in C.  Subpart slots may identify structural, functional, or similar
kinds of relationships among components."

  :def (and (value-type ?x HAS-ATTRIBUTE attribute-slot)
            (value-type ?x HAS-SUBPART subpart-slot)
            (value-type ?x HAS-CONSTRAINT constraint)
            (value-type ?x SATISFIES-CONSTRAINT constraint)))

and here is its specialization in theory vt-design:

(define-class VT-COMPONENT (?component)
 "A VT component is just a component as defined
by the configuration-design ontology, except that we define a slot
for the cost."
  :def (and (component ?component)
            (value-type ?component HAS-CONSTRAINT vt-constraint)
            (has-attribute ?component COMPONENT.COST)
            (cost-quantity (COMPONENT.COST ?component)))

  :issues (("Why not include the sum of subparts in the cost metric?"
           "That assumes linear combination function for cost, which
            is a domain specific assumption.")))

In this case we named a subclass of component that has the restriction
that its HAS-CONSTRAINT slot has the value type vt-constraint.
There is also a way to specialize functions polymorphically, without
renaming them, as in these definitions.

;; FROM PARENT THEORY PHYSICAL-QUANTITIES
(define-function * (?x ?y):-> ?z

  "Multiplication for physical-quantities.  The '*' operator for
complex numbers (part of KIF specification) is overloaded to operate
on physical quantities.  This operator is further defined for quantity
subclasses.  The dimension of the product is the product of the
dimensions of the multipled quantities."

  :when (and (physical-quantity ?x)
	     (physical-quantity ?y))
  :def (and (physical-quantity ?z)
            (= (dimension ?z) 
               (* (dimension ?x) (dimension ?y))))

  :axiom-def (distributes * + physical-quantity))
		  
;; FROM CHILD THEORY SCALAR-QUANTITIES:
(define-function * (?x ?y) :-> ?z

  "* defines the specialization of the QUANTITY
multiplication operator * for scalar-quantitys.  The operator enforces the
relationship between the physical-dimensions of the operands and the
product.  The operator is defined in terms of the number
multiplication operator * and the magnitudes of quantities for a
particular unit.  Scalar-Quantitys excluding all the zero-scalars form an
abelian group with respect to this operator and the identity-scalar
<1>.  This operator distributes over the + operator for scalar-quantitys,
providing a field behavior with restrictions."

  :when (and (scalar-quantity ?x)
             (scalar-quantity ?y))
  :def (and (scalar-quantity ?z)
            (forall (?u ?u1 ?u2)
                    (=> (and (unit-of-measure ?u)
                             (unit-of-measure ?u1)
                             (unit-of-measure ?u2)
                             (= ?u (* ?u1 ?u2)))
                        (= (* (magnitude ?x ?u1) 
                              (magnitude ?y ?u2))
                           (magnitude ?z ?u)))))
  :axiom-def (abelian-group 
               (kappa (?x)
                      (and (scalar-quantity ?x) 
                           (forall ?dim 
                                   (=> (physical-dimension ?dim)
                                       (/= (zero-scalar-for-dimension ?dim) 
                                           ?x)))))
               *
               1))


Editor's postscript:  
   Ontolingua doesn't do any checking that included definitions are
   consistent with the other definitions in a theory.  That is the job of
   a reasoning engine of some sort.  Maybe you could do that with Epikit,
   but the general case is intractable.

   KIF desperately needs a theory/context mechanism (more than set
   inclusion).  There is some research going on that might be
   applicable.  Ontolingua has the theory scheme as a common
   denominator, as a simple modularity mechanism for mutually
   consistent ontologies.  It is not a namespace mechanism.

tom