Function INVERSE

• Defined in theory: Kif-relations
• Source code: frame-ontology.lisp

Slots on this function:

Documentation:

One binary relation is the inverse of another if they are equivalent when their arguments are swapped.

Instance-Of: Function

Arity: 2

Domain: Binary-relation

Range: Binary-relation

Equivalence Axioms:

(<=> (Holds ?Binary-Relation ?X ?Y)
     (Holds (Inverse ?Binary-Relation) ?Y ?X))

Other Related Axioms:

(Inherited-Facet-Value Slot-Cardinality One-One Inverse 1)

(Inherited-Facet-Value Slot-Value-Type One-One Inverse Function)

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

(Inherited-Facet-Value Slot-Cardinality One-Many Inverse 1)

(Inherited-Facet-Value Slot-Value-Type One-Many Inverse Function)

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

(Instance-Of (Function (Inverse ?R)) Not)

(Not (Function (Inverse ?R)))

(<=> (Many-Many ?R)
     (And (Binary-Relation ?R)
          (Not (Function ?R))
          (Not (Function (Inverse ?R)))))

(<- (Inverse ?Binary-Relation)
    (If (Binary-Relation ?Binary-Relation)
        (Setofall (Listof ?Y ?X) (Holds ?Binary-Relation ?X ?Y))))

(<=> (Holds ?Binary-Relation ?X ?Y)
     (Holds (Inverse ?Binary-Relation) ?Y ?X))

Notes:

• Note that INVERSE is a function. It is possible to have more than one relation constant naming the inverse of a relation, but they are all = to each other.