Relation Composition-Of

• Defined in ontology: Frame-ontology
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/ontolingua/../../all-ontologies/ontolingua/frame-ontology.lisp

Arity: 2

Documentation:

A binary relation R is a COMPOSITION-OF a sequence of binary relations R_1, R_2, ... R_N iff there exists a relation R' that is a COMPOSITION-OF the sequence R_1 ... R_{N-1}, and R is the (COMPOSITION R_1 R').

Relations are composed right to left. For example, if (composition-of R (listof a b c d)) then R = (composition d (composition c (composition b a))).

When the relations are unary functions, the sequence corresponds to nested parentheses in functional notation. For example, if F is composition-of functions a, b, and c, (COMPOSITION-OF F (listof a b c)) means (f ?x) is equal to (a (b (c ?x))).

Notes:

• Example: (=> (composition-of r (listof a b c d)) (= r (composition d (composition c (composition b a)))))
  
  

• version 4: new slot on relations
• Commented-out: ;; (composition-of a (listof a)) ;; (composition-of (composition b a) (listof a b)) ;; (composition-of R (listof a b c d)) => ;; R = (composition d (composition c (composition b a)))

Domain: Binary-Relation

Instance-Of: Binary-Relation, Relation, Set

Range: List

Implication Axioms for Composition-Of:

(=> (Composition-Of ?Binary-Relation ?List-Of-Relations)
    (Or (And (Single ?List-Of-Relations)
             (= ?Binary-Relation (First ?List-Of-Relations)))
        (And (Double ?List-Of-Relations)
             (= ?Binary-Relation
                (Composition (First (Rest ?List-Of-Relations))
                             (First ?List-Of-Relations))))
        (Exists (?Left-Sub-Relation)
                (And (= ?Binary-Relation
                        (Composition (Last ?List-Of-Relations)
                                     ?Left-Sub-Relation))
                     (Composition-Of ?Left-Sub-Relation
                                     (Butlast ?List-Of-Relations))))))

(=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))

Equivalence Axioms for Composition-Of:

(<=> (Composition-Of ?Binary-Relation ?List-Of-Relations)
     (And (Binary-Relation ?Binary-Relation)
          (List ?List-Of-Relations)
          (Not (Null ?List-Of-Relations))
          (=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))
          (Or (And (Single ?List-Of-Relations)
                   (= ?Binary-Relation (First ?List-Of-Relations)))
              (And (Double ?List-Of-Relations)
                   (= ?Binary-Relation
                      (Composition (First (Rest ?List-Of-Relations))
                                   (First ?List-Of-Relations))))
              (Exists (?Left-Sub-Relation)
                      (And (= ?Binary-Relation
                              (Composition (Last ?List-Of-Relations)
                                           ?Left-Sub-Relation))
                           (Composition-Of ?Left-Sub-Relation
                                           (Butlast ?List-Of-Relations)))))))

Axioms for Composition-Of:

(Not (Null ?List-Of-Relations))

(List ?List-Of-Relations)

(Binary-Relation ?Binary-Relation)

Implication Axioms mentioning Composition-Of:

(=> (= (Compose @Binary-Relations) ?Composed-Relation)
    (Composition-Of ?Composed-Relation (Listof @Binary-Relations)))

Equivalence Axioms mentioning Composition-Of:

(<=> (Compose @Binary-Relations)
     (Composition-Of ?Composed-Relation (Listof @Binary-Relations)))