Relation Has-Value-Of-Type

Instance-Of: Relation, Set
Subrelation-Of: Value-Type
Arity: 3
Documentation:
A binary relation R HAS-VALUE-OF-TYPE T on domain instance d if there exists a v such that R(d,v) and v is an instance of T.

Notes:


Implication Axioms for Has-Value-Of-Type:

(=> (Has-Value-Of-Type ?Instance ?Binary-Relation ?Type)
    (Value-Type ?Instance ?Binary-Relation ?Type))


Equivalence Axioms for Has-Value-Of-Type:

(<=> (Has-Value-Of-Type ?Instance ?Binary-Relation ?Type)
     (And (Binary-Relation ?Binary-Relation)
          (Class ?Type)
          (>= (Value-Cardinality ?Instance ?Binary-Relation) 1)
          (Value-Type ?Instance ?Binary-Relation ?Type)))


Axioms for Has-Value-Of-Type:

(>= (Value-Cardinality ?Instance ?Binary-Relation) 1)

(Binary-Relation ?Binary-Relation)

(Nth-Domain Has-Value-Of-Type 3 Class)

(Nth-Domain Has-Value-Of-Type 2 Binary-Relation)


Implication Axioms mentioning Has-Value-Of-Type:

(=> (Has-Slot-Value-Of-Type ?Domain-Class ?Relation ?Type)
    (=> (Instance-Of ?Instance ?Domain-Class)
        (Has-Value-Of-Type ?Instance ?Relation ?Type)))


Equivalence Axioms mentioning Has-Value-Of-Type:

(<=> (Has-Slot-Value-Of-Type ?Domain-Class ?Relation ?Type)
     (And (Class ?Domain-Class)
          (Binary-Relation ?Relation)
          (Class ?Type)
          (=> (Instance-Of ?Instance ?Domain-Class)
              (Has-Value-Of-Type ?Instance ?Relation ?Type))))