Function All-Inherited-Slot-Values

Arity: 3
Documentation:
The all-inherited-slot-values of binary relation R on class C is the set V of values for which R(c,s) holds on each instance i of C and member v of V. Unlike inherited-slot-values, there may not exist any other value v_i for which R(i,v_i) holds. Inherited values are monotonic, not default.
Instance-Of: Function, Relation, Set

Equivalence Axioms for All-Inherited-Slot-Values:

(<=> (All-Inherited-Slot-Values ?Class ?Binary-Relation)
     (And (Class ?Class)
          (Binary-Relation ?Binary-Relation)
          (Forall (?Instance ?Value)
                  (=> (Instance-Of ?Instance ?Class)
                      (<=> (Member ?Value ?Set-Of-Values)
                           (Holds ?Binary-Relation ?Instance ?Value))))))


Axioms for All-Inherited-Slot-Values:

(Nth-Domain All-Inherited-Slot-Values 2 Binary-Relation)

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


Implication Axioms mentioning All-Inherited-Slot-Values:

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

(=> (= (All-Inherited-Slot-Values ?Class ?Binary-Relation)
       ?Set-Of-Values)
    (Binary-Relation ?Binary-Relation))

(=> (= (All-Inherited-Slot-Values ?Class ?Binary-Relation)
       ?Set-Of-Values)
    (Class ?Class))