Class BINARY-RELATION


Slots on this class:

Documentation:
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.
Instance-Of: Class
Subclass-Of: Relation
Domain-Of: Inverse
Range-Of: Inverse
Superclass-Of:
Many-many, Many-one, One-many, One-one, Unary-function


Slots on instances of this class:

Arity: 2

Equivalence Axioms:

(<=> (Binary-Relation ?Relation)
     (And (Relation ?Relation)
          (Not (Empty ?Relation))
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation) (Double ?Tuple)))))


Axioms:

(Forall (?Tuple) (=> (Member ?Tuple ?Relation) (Double ?Tuple)))

(Not (Empty ?Relation))

(Relation ?Relation)


Other Related Axioms:

(<=> (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)