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.
(<=> (Instance-Of ?Individual ?Class)
(And (Class ?Class) (Holds ?Class ?Individual)))
(Instance-Of Class Class)
(Instance-Of Thing Class)
(Instance-Of Individual-Thing Class)
(Instance-Of Inherited-Through-Class-Of-Relation Class)
(<= (Instance-Of $Arg1 $Class2)
(And (Instance-Of $Arg1 $Class1) (Subclass-Of $Class1 $Class2)))
(=> (Instance-Of $X $Y) (Class $Y))
(<=> (Instance-Of ?Individual ?Class)
(Member (Listof ?Individual) ?Class))
(<=> (Instance-Of ?Individual ?Class)
(And (Class ?Class) (Holds ?Class ?Individual)))
(Instance-Of Has-Instance Relation)
(<=> (Has-Instance $Arg1 $Arg2) (Instance-Of $Arg2 $Arg1))
(Inverse Has-Instance Instance-Of)
(Instance-Of All-Instances Function)
(=> (= (All-Instances ?Class) ?Set-Of-Instances)
(Forall (?Instance)
(<=> (Member ?Instance ?Set-Of-Instances)
(Instance-Of ?Instance ?Class))))
(Instance-Of (Arity One-Of) Undefined)
(Instance-Of One-Of Function)
(=> (= (One-Of @Members) ?Class)
(Forall (?Instance)
(<=> (Instance-Of ?Instance ?Class)
(Member ?Instance (Setof @Members)))))
(Instance-Of Subclass-Of Relation)
(<=> (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)))))
(Instance-Of Superclass-Of Relation)
(Instance-Of Subrelation-Of Relation)
(Instance-Of Direct-Instance-Of Relation)
(Subrelation-Of Direct-Instance-Of Instance-Of)
(=> (Direct-Instance-Of ?Individual ?Class)
(<= (Not (Exists (?Other-Class)
(And (Not (= ?Other-Class ?Class))
(Instance-Of ?Individual ?Other-Class)
(Subclass-Of ?Other-Class ?Class))))
(Not (Provable (Not (Not (Exists (?Other-Class)
(And (Not (= ?Other-Class
?Class))
(Instance-Of
?Individual
?Other-Class)
(Subclass-Of
?Other-Class
?Class)))))))))
(Instance-Of Direct-Subclass-Of Relation)
(Instance-Of Arity Function)
(Instance-Of Exact-Domain Function)
(Instance-Of Exact-Range Function)
(Instance-Of Total-On Relation)
(Instance-Of Onto Relation)
(Instance-Of Projection Function)
(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance))))))
(Instance-Of Composition-Of Relation)
(Instance-Of (Arity Compose) Undefined)
(Instance-Of Compose Function)
(Instance-Of Alias Relation)
(Instance-Of Domain Relation)
(Instance-Of Domain-Of Relation)
(Instance-Of Range Relation)
(Instance-Of Range-Of Relation)
(Instance-Of Nth-Domain Relation)
(<=> (Nth-Domain ?Relation ?N ?Type)
(And (Defined (Arity ?Relation))
(Positive-Integer ?N)
(Class ?Type)
(Forall (?Tuple)
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Instance-Of (Nth ?Tuple ?N) ?Type))))))
(Instance-Of Relation-Universe Function)
(=> (= (Relation-Universe ?Relation) ?Type-Class)
(Forall (?X)
(<=> (Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(Item ?X ?Tuple)))
(Instance-Of ?X ?Type-Class))))
(Instance-Of Has-Value Relation)
(Instance-Of All-Values Function)
(Instance-Of Value-Type Relation)
(<=> (Value-Type ?Instance ?Binary-Relation ?Type)
(And (Binary-Relation ?Binary-Relation)
(Class ?Type)
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))))
(Instance-Of Same-Values Relation)
(Instance-Of Value-Cardinality Function)
(Instance-Of Minimum-Value-Cardinality Relation)
(Instance-Of Maximum-Value-Cardinality Relation)
(Instance-Of Slot-Value-Type Relation)
(<=> (Slot-Value-Type ?Class ?Binary-Relation ?Type)
(And (Class ?Class)
(Binary-Relation ?Binary-Relation)
(Class ?Type)
(Forall (?Instance)
(=> (Instance-Of ?Instance ?Class)
(=> (Holds ?Binary-Relation
?Instance
?Slot-Value)
(Instance-Of ?Slot-Value ?Type))))))
(Instance-Of Slot-Cardinality Function)
(=> (= (Slot-Cardinality ?Domain-Class ?Binary-Relation) ?N)
(=> (Instance-Of ?Instance ?Domain-Class)
(= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))
(Instance-Of Minimum-Slot-Cardinality Relation)
(<=> (Minimum-Slot-Cardinality ?Domain-Class ?Relation ?N)
(=> (Instance-Of ?Instance ?Domain-Class)
(>= (Value-Cardinality ?Instance ?Relation) ?N)))
(Instance-Of Maximum-Slot-Cardinality Relation)
(<=> (Maximum-Slot-Cardinality ?Domain-Class ?Relation ?N)
(=> (Instance-Of ?Instance ?Domain-Class)
(=< (Value-Cardinality ?Instance ?Relation) ?N)))
(Instance-Of Single-Valued-Slot Relation)
(<=> (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 Inherited-Slot-Value Relation)
(<=> (Inherited-Slot-Value ?Class ?Binary-Relation ?Value)
(And (Class ?Class)
(Binary-Relation ?Binary-Relation)
(Forall (?Instance ?Value)
(=> (Instance-Of ?Instance ?Class)
(Holds ?Binary-Relation ?Instance ?Value)))))
(Instance-Of All-Inherited-Slot-Values Function)
(=> (= (All-Inherited-Slot-Values ?Class ?Binary-Relation)
?Set-Of-Values)
(Forall (?Instance ?Value)
(=> (Instance-Of ?Instance ?Class)
(<=> (Member ?Value ?Set-Of-Values)
(Holds ?Binary-Relation ?Instance ?Value)))))
(Instance-Of Same-Slot-Values Relation)
(<=> (Same-Slot-Values ?Class ?Slot1 ?Slot2)
(And (Class ?Class)
(Binary-Relation ?Slot1)
(Binary-Relation ?Slot2)
(Forall (?Instance ?Value)
(=> (Instance-Of ?Instance ?Class)
(<=> (Holds ?Slot1 ?Instance ?Value)
(Holds ?Slot2 ?Instance ?Value))))))
(Instance-Of Inherited-Facet-Value Relation)
(<=> (Inherited-Facet-Value ?Facet ?Class ?Binary-Relation ?Value)
(And (Class ?Class)
(Binary-Relation ?Binary-Relation)
(Forall (?Instance ?Value)
(=> (Instance-Of ?Instance ?Class)
(Holds ?Facet
?Instance
?Binary-Relation
?Value)))))
(Forall (?C1 ?C2)
(=> (And (Member ?C1 ?Set-Of-Classes)
(Member ?C2 ?Set-Of-Classes)
(Not (= ?C1 ?C2)))
(Forall (?I)
(=> (Instance-Of ?I ?C1)
(Not (Instance-Of ?I ?C2))))))
(Instance-Of Class-Partition Class)
(<=> (Class-Partition ?Set-Of-Classes)
(And (Set ?Set-Of-Classes)
(Forall (?C) (=> (Member ?C ?Set-Of-Classes) (Class ?C)))
(Forall (?C1 ?C2)
(=> (And (Member ?C1 ?Set-Of-Classes)
(Member ?C2 ?Set-Of-Classes)
(Not (= ?C1 ?C2)))
(Forall (?I)
(=> (Instance-Of ?I ?C1)
(Not (Instance-Of ?I ?C2))))))))
(Instance-Of Subclass-Partition Relation)
(Instance-Of Exhaustive-Subclass-Partition Relation)
(<=> (Exhaustive-Subclass-Partition ?C ?Class-Partition)
(And (Subclass-Partition ?C ?Class-Partition)
(Forall (?Instance)
(=> (Instance-Of ?Instance ?C)
(Exists (?Subclass)
(And (Member ?Subclass
?Class-Partition)
(Member ?Instance ?Subclass)))))))
(Instance-Of Symmetric-Relation Class)
(Instance-Of Antisymmetric-Relation Class)
(Instance-Of Asymmetric-Relation Class)
(=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X ?X))
(Instance-Of Reflexive-Relation Class)
(<=> (Reflexive-Relation ?R)
(And (Binary-Relation ?R)
(=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X ?X))))
(Instance-Of Irreflexive-Relation Class)
(Instance-Of Transitive-Relation Class)
(Instance-Of Weak-Transitive-Relation Class)
(Instance-Of One-To-One-Relation Class)
(Instance-Of Many-To-One-Relation Class)
(Instance-Of One-To-Many-Relation Class)
(Instance-Of (Function (Inverse ?R)) Not)
(Instance-Of (Function ?R) Not)
(Instance-Of Many-To-Many-Relation Class)
(Instance-Of Equivalence-Relation Class)
(Instance-Of Partial-Order-Relation Class)
(=> (And (Instance-Of ?X (Exact-Domain ?R))
(Instance-Of ?Y (Exact-Domain ?R)))
(Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))
(Instance-Of Total-Order-Relation 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)))))
(Instance-Of Documentation Relation)
(Instance-Of Related-Axioms Relation)
Because instance-of is in common usage, and member-of can get confused with the set and list operators.
Because these words are used to mean many different things in different contexts.
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.