A binary relation maps instances of a class to instances of another class. Its arity is 2. Binary relations are often shown as slots in frame systems.
(<=> (Binary-Relation ?Relation) (And (Relation ?Relation) (Not (Empty ?Relation)) (Forall (?Tuple) (=> (Member ?Tuple ?Relation) (Double ?Tuple)))))
(Forall (?Tuple) (=> (Member ?Tuple ?Relation) (Double ?Tuple))) (Not (Empty ?Relation)) (Relation ?Relation)
(<=> (One-One ?R) (And (Binary-Relation ?R) (Function ?R) (Value-Type ?R Inverse Function) (Value-Cardinality ?R Inverse 1))) (<=> (Many-One ?R) (And (Binary-Relation ?R) (Function ?R))) (<=> (One-Many ?R) (And (Binary-Relation ?R) (Value-Type ?R Inverse Function) (Value-Cardinality ?R Inverse 1))) (<=> (Many-Many ?R) (And (Binary-Relation ?R) (Not (Function ?R)) (Not (Function (Inverse ?R))))) (<=> (Unary-Function ?F) (And (Function ?F) (Binary-Relation ?F))) (<= (Arity $X 2) (Binary-Relation $X)) (=> (Binary-Relation ?Relation) (= (Arity ?Relation) 2)) (<=> (Binary-Relation ?Relation) (And (Relation ?Relation) (Not (Empty ?Relation)) (Forall (?Tuple) (=> (Member ?Tuple ?Relation) (Double ?Tuple))))) (<- (Inverse ?Binary-Relation) (If (Binary-Relation ?Binary-Relation) (Setofall (Listof ?Y ?X) (Holds ?Binary-Relation ?X ?Y)))) (<- (Composition ?R1 ?R2) (If (And (Binary-Relation ?R1) (Binary-Relation ?R2)) (Setofall (Listof ?X ?Z) (Exists (?Y) (And (Holds ?R1 ?X ?Y) (Holds ?R2 ?Y ?Z)))))) (Nth-Domain Composition 3 Binary-Relation) (Nth-Domain Composition 2 Binary-Relation) (Nth-Domain Composition 1 Binary-Relation)