The VALUE-TYPE of a binary relation R with respect to a given instance d is a constraint on the values of R when R is applied to d. The constraint is specified as a class T such that when R(d,t) holds, t is an instance of T.
(<=> (Value-Type ?Instance ?Binary-Relation ?Type)
(And (Binary-Relation ?Binary-Relation)
(Class ?Type)
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))))
(Nth-Domain Value-Type 3 Class) (Nth-Domain Value-Type 2 Binary-Relation)
(<=> (Value-Type ?Instance ?Binary-Relation ?Type)
(And (Binary-Relation ?Binary-Relation)
(Class ?Type)
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))))
(<=> (One-To-One-Relation ?R)
(And (Unary-Function ?R)
(Value-Type ?R Inverse Function)
(Value-Cardinality ?R Inverse 1)))
(<=> (One-To-Many-Relation ?R)
(And (Binary-Relation ?R)
(Value-Type ?R Inverse Function)
(Value-Cardinality ?R Inverse 1)))