Relation Value-Type

Arity: 3
Documentation:
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.

Notes:

  • VALUE-TYPE is convenient for specifying type restrictions on slots relative to a class by using the class's instance variable.
  • See-Also: slot-value-type
Has-Subrelation: Has-One-Of-Type@Ol-User%Slot-Constraint-Sugar, Has-Value-Of-Type@Ol-User%Slot-Constraint-Sugar
Instance-Of: Relation, Set

Implication Axioms for Value-Type:

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

Equivalence Axioms for Value-Type:

(<=> (Value-Type ?Instance ?Binary-Relation ?Type)
     (And (Binary-Relation ?Binary-Relation)
          (Class ?Type)
          (Forall (?Value)
                  (=> (Holds ?Binary-Relation ?Instance ?Value)
                      (Instance-Of ?Value ?Type)))))

Axioms for Value-Type:

(Binary-Relation ?Binary-Relation)

(Nth-Domain Value-Type 3 Class)

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

Implication Axioms mentioning Value-Type:

(=> (Has-Value-Of-Type@Ol-User%Slot-Constraint-Sugar ?Instance
                       ?Binary-Relation
                       ?Type)
    (Value-Type ?Instance ?Binary-Relation ?Type))

(=> (Has-One-Of-Type@Ol-User%Slot-Constraint-Sugar ?Instance
                     ?Binary-Relation
                     ?Type)
    (Value-Type ?Instance ?Binary-Relation ?Type))

Equivalence Axioms mentioning 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)))

(<=> (One-One ?R)
     (And (Binary-Relation ?R)
          (Function ?R)
          (Value-Type ?R Inverse Function)
          (Value-Cardinality ?R Inverse 1)))

(<=> (One-Many ?R)
     (And (Binary-Relation ?R)
          (Value-Type ?R Inverse Function)
          (Value-Cardinality ?R Inverse 1)))

(<=> (Funterm ?Expr)
     (And (Term ?Expr)
          (List ?Expr)
          (Value-Type ?Expr First Funconst)
          (Value-Cardinality ?Expr First 1)))

Axioms mentioning Value-Type:

(<= (Value-Type Ontolingua-Internal::@Arg-List)
    (Has-Value-Of-Type@Ol-User%Slot-Constraint-Sugar Ontolingua-Internal::@Arg-List))

(<= (Value-Type Ontolingua-Internal::@Arg-List)
    (Has-One-Of-Type@Ol-User%Slot-Constraint-Sugar Ontolingua-Internal::@Arg-List))