Function ALL-INSTANCES

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

Slots on this function:

Documentation:

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.

Instance-Of: Function

Arity: 2

Domain: Class

Range: Set

Equivalence Axioms:

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

Other Related Axioms:

(=> (All-Instances $X $Y) (Set $Y))

(=> (All-Instances $X $Y) (Class $X))

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

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

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

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