Relation Subrelation-Of

Arity: 2
Documentation:
A relation R is a subrelation-of relation R' if, viewed as sets, R is a subset of R'. In other words, every tuple of R is also a tuple of R'. In some more words, if R holds for some arguments arg_1, arg_2, ... arg_n, then R' holds for the same arguments. Thus, a relation and its subrelation must have the same arity, which could be undefined.

In CycL, subrelation-of is called #%genlSlots.

Notes:

  • Do the arities of the relations have to match?

    No. Used to be defined this way, but it was an unnecessary restriction. If the parent relation has a (fixed) arity, then the child's arity must be equal to it. However, the child could be of fixed arity and the parent undefined (variable) arity.

Domain: Relation
Instance-Of: Binary-Relation, Relation, Set
Inverse: Has-Subrelation
Range: Relation

Implication Axioms for Subrelation-Of:

(=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
    (=> (Defined (Arity ?Parent-Relation))
        (= (Arity ?Child-Relation) (Arity ?Parent-Relation))))

(=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
    (Forall (?Tuple)
            (=> (Member ?Tuple ?Child-Relation)
                (Member ?Tuple ?Parent-Relation))))


Equivalence Axioms for Subrelation-Of:

(<=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
     (And (Relation ?Child-Relation)
          (Relation ?Parent-Relation)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Child-Relation)
                      (Member ?Tuple ?Parent-Relation)))))

(<=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
     (=> (Holds ?Child-Relation @Arguments)
         (Holds ?Parent-Relation @Arguments)))


Axioms for Subrelation-Of:

(Relation ?Parent-Relation)

(Relation ?Child-Relation)


Frame References to Subrelation-Of:

In relation Must-Be-One-Of@Ol-User%Slot-Constraint-Sugar:

Subrelation-Of: Can-Be-One-Of@Ol-User%Slot-Constraint-Sugar

In relation Direct-Subclass-Of:

Subrelation-Of: Subclass-Of

In relation Exhaustive-Subclass-Partition:

Subrelation-Of: Subclass-Partition

In relation Proper-Subset:

Subrelation-Of: Subset

In relation Has-One-Of-Type@Ol-User%Slot-Constraint-Sugar:

Subrelation-Of: Value-Type

In relation Has-Single-Slot-Value-Of-Type@Ol-User%Slot-Constraint-Sugar:

Subrelation-Of: Has-Slot-Value-Of-Type@Ol-User%Slot-Constraint-Sugar
...

Equivalence Axioms mentioning Subrelation-Of:

(<=> (Total-On ?Relation ?Domain-Relation)
     (Subrelation-Of (Exact-Domain ?Relation) ?Domain-Relation))