Class Class

Arity: 1
Inherited-Slot-Value: 1
A class can be thought of as a collection of individuals. Formally, a class is a unary relation, a set of tuples (lists) of length one. Each tuple contains an object which is said to be an instance of the class. An individual, or object, is any identifiable entity in the universe of discourse (anything that can be denoted by a object constant in KIF), including classes themselves.

The notion of CLASS is introduced in addition to the relation vocabulary because of the importance of classes and types in knowledge representation practice. The notion of class and relation are merged to unify relational and object-centered representational conventions. Classes serve the role of `sorts' and `types'.

There is no first-order distinction between classes and unary relations. One is free to define a second-order predicate that makes the distinction. For example, (predicate C) could mean that the unary relation C should be thought of more as a property than as a collection of individuals over which one might quantify some statement. Logically, all such predicates would still be instances of the metaclass CLASS.

The fact that an object i is an instance of class C is denoted by the sentence (C i). One may also use the equivalent form (INSTANCE-OF i C). This is not equivalent to (MEMBER i C).
An instance of a class is not a set-ontologetic member of the class; rather, the tuple containing the instance is a element of the set of tuples which is a relation.

The definition of a class is a predicate over a single free variable, such that the predicate holds for instances of the class. In other words, classes are defined intentionally. Two separately-defined classes may have the same extension (in this case they are = to each other). It is possible to define a class by enumerating its instances, using KIF's set operations. For example, (define-class primary-color (?color)

:iff-def (member ?color (setof red green blue)))


  • See-Also: In CycL, classes are called collections.

    In Loom, classes are called concepts.

    In KEE, classes are called classes.

    In Epikit, classes are not explicitly part of the language but are conventionally denoted by unary relations, or using a binary relation such as (ISA <instance> <class> ).

All-Instances, Subclass-Of, Subclass-Partition, Visible-Slots-For-Query@Interface-Ontology
Complex-Number, Negative, Positive, Show-All-Values-Slot@Interface-Ontology, Zero ...
Instance-Of: Class, Relation, Set
Domain, Exact-Range, Range, Relation-Universe, Subclass-Of ...
Subclass-Of: Relation, Set
Superclass-Of: Integer-Range@Ranges, Real-Range@Ranges


Arity: 1

Equivalence Axioms for Class:

(<=> (Class ?Class) (And (Relation ?Class) (= (Arity ?Class) 1)))

Implication Axioms mentioning Class:

(=> (Inherited-Through-Class-Of-Relation ?R)
    (=> (And (Holds ?R ?X ?C1)
             (Class ?C1)
             (Class ?C2)
             (Subclass-Of ?C2 ?C1))
        (Holds ?R ?X ?C2)))

(=> (Class-Partition ?Set-Of-Classes)
    (Forall (?C) (=> (Member ?C ?Set-Of-Classes) (Class ?C))))

(=> (= (All-Instances ?Class) ?Set-Of-Instances) (Class ?Class))

(=> (= (Exact-Range ?Relation) ?Range-Class) (Class ?Range-Class))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Class ?Projection-Relation))

Equivalence Axioms mentioning Class:

(<=> (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)))))

(<=> (Inherited-Through-Class-Of-Relation ?R)
     (And (Binary-Relation ?R)
          (=> (And (Holds ?R ?X ?C1)
                   (Class ?C1)
                   (Class ?C2)
                   (Subclass-Of ?C2 ?C1))
              (Holds ?R ?X ?C2))))

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

(<=> (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 Class:

(Nth-Domain Slot-Cardinality 1 Class)

(Nth-Domain Nth-Domain 3 Class)

(Nth-Domain Value-Type 3 Class)

(Nth-Domain Same-Slot-Values 1 Class)

(Nth-Domain All-Inherited-Slot-Values 1 Class)