Function ALL-INSTANCES

The instances of some classes may be specified extensionally. That is, one can list all of the instances of the class by definition. For this case we say (= (all-instances C) (setof V_1 V_2 ... V_n)), where C is a class and the V_i are its instances.

ALL-INSTANCES imposes a monotonic constraint. Any subclass of C cannot have any instances outside of the ALL-INSTANCES of C. Note that this is not indexical or modal: whether something is in all-instances is a property of the modeled world and does not depend on the facts currently stored in some knowledge base.

Arity: 2

Domain: Class

Range: Set

Axioms:

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

• Defined in theory: Frame-ontology
• Source code: frame-ontology.lisp

Notes:

• Is all-instances the inverse of instance-of?

  No. Instance-of maps indivdual instances to classes, whereas all-instances maps classes to sets of instances.

• The name all-instances is borrowed from Cyc.
• Example: (all-instances truth-values (setof true false))