Relation Instance-Of

• Defined in ontology: Frame-ontology
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/ontolingua/../../all-ontologies/ontolingua/frame-ontology.lisp
• Also defined in: Interface-ontology

Arity: 2

Definition-Sort-Index@Interface-Ontology: 550

Documentation:

An object is an instance-of a class if it is a member of the set denoted by that class. One would normally state the fact that individual i is an instance of class C with with the relational form (C i), but it is equivalent to say (INSTANCE-OF i C). Instance-of is useful for defining the second-order relations and classes that are about class/instance networks.

An individual may be an instance of many classes, some of which may be subclasses of others. Thus, there is no assumption in the meaning of instance-of about specificity or uniqueness. See DIRECT-INSTANCE-OF.

Notes:

• Why not call instance-of `member-of'?

  Because instance-of is in common usage, and member-of can get confused with the set and list operators.

• Why not call instance-of `example-of', or `isa'?

  Because these words are used to mean many different things in different contexts.

• See-Also: In Cyc, instance-of is called #%allInstanceOf.

  In KEE, instance-of is called member.of.

  In Loom, instance-of is implicit in the syntax (unary predicates).

  In Epikit, there is no notion of instances, although by convention people use unary relations to denote instance-of relationships.

• See-Also: direct-instance-of

Has-Subrelation: Direct-Instance-Of

Instance-Of:

Binary-Relation, Binary-Relation, Inherited-Through-Class-Of-Relation, Relation, Relation ...

Inverse: Has-Instance

Range: Class

Implication Axioms for Instance-Of:

(=> (Instance-Of ?Individual ?Class) (Holds ?Class ?Individual))

Equivalence Axioms for Instance-Of:

(<=> (Instance-Of ?Individual ?Class)
     (And (Class ?Class) (Holds ?Class ?Individual)))

(<=> (Instance-Of ?Individual ?Class)
     (Member (Listof ?Individual) ?Class))

Frame References to Instance-Of:

In relation Nth-Domain:

Instance-Of: Relation

In relation Composition-Of:

Instance-Of: Binary-Relation, Relation

In function First:

Instance-Of: Binary-Relation, Function

In function Ceiling:

Instance-Of: Binary-Relation, Function

In relation Same-Slot-Values:

Instance-Of: Relation

In class Double:

Instance-Of: Class

Implication Axioms mentioning Instance-Of:

(=> (= (All-Instances ?Class) ?Set-Of-Instances)
    (Forall (?Instance)
            (<=> (Member ?Instance ?Set-Of-Instances)
                 (Instance-Of ?Instance ?Class))))

(=> (= (One-Of @Members) ?Class)
    (Forall (?Instance)
            (<=> (Instance-Of ?Instance ?Class)
                 (Member ?Instance (Setof @Members)))))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Forall (?Projection-Instance)
            (<=> (Instance-Of ?Instance ?Projection-Relation)
                 (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (= (Nth ?Tuple ?Column) ?Instance))))))

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Forall (?X)
            (<=> (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (Item ?X ?Tuple)))
                 (Instance-Of ?X ?Type-Class))))

(=> (= (Slot-Cardinality ?Domain-Class ?Binary-Relation) ?N)
    (=> (Instance-Of ?Instance ?Domain-Class)
        (= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

Equivalence Axioms mentioning Instance-Of:

(<=> (All-Instances ?Class)
     (And (Class ?Class)
          (Set ?Set-Of-Instances)
          (Forall (?Instance)
                  (<=> (Member ?Instance ?Set-Of-Instances)
                       (Instance-Of ?Instance ?Class)))))

(<=> (Subclass-Of ?Child-Class ?Parent-Class)
     (And (Class ?Parent-Class)
          (Class ?Child-Class)
          (Forall (?Instance)
                  (=> (Instance-Of ?Instance ?Child-Class)
                      (Instance-Of ?Instance ?Parent-Class)))))

(<=> (Total-Order-Relation ?R)
     (And (Partial-Order-Relation ?R)
          (=> (And (Instance-Of ?X (Exact-Domain ?R))
                   (Instance-Of ?Y (Exact-Domain ?R)))
              (Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))))

(<=> (One-Of @Members)
     (Forall (?Instance)
             (<=> (Instance-Of ?Instance ?Class)
                  (Member ?Instance (Setof @Members)))))

(<=> (Single-Valued-Slot ?Class ?Binary-Relation)
     (And (Class ?Class)
          (Binary-Relation ?Binary-Relation)
          (=> (Instance-Of ?Instance ?Class)
              (=> (Holds ?Binary-Relation ?Instance ?Slot-Value1)
                  (Holds ?Binary-Relation ?Instance ?Slot-Value2)
                  (= ?Slot-Value1 ?Slot-Value2)))))

Axioms mentioning Instance-Of:

(<= (Instance-Of Ontolingua-Internal::@Arg-List)
    (Direct-Instance-Of Ontolingua-Internal::@Arg-List))

(Instance-Of 0 Zero)

(Instance-Of 'Quote Termop)

(Instance-Of 'Cond Termop)

(Instance-Of 'Listof Termop)