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
(=> (Instance-Of ?Individual ?Class) (Holds ?Class ?Individual))
(<=> (Instance-Of ?Individual ?Class) (And (Class ?Class) (Holds ?Class ?Individual))) (<=> (Instance-Of ?Individual ?Class) (Member (Listof ?Individual) ?Class))
(=> (= (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)))
(<=> (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)))))
(<= (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)