Function Composition

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

Instance-Of@Frame-Ontology: Function, Relation, Set

Arity@Frame-Ontology: 3

Documentation@Ol%Frame-Ontology:

The composition of binary relations R_1 and R_2 is a relation R_3 such that R_1(x,y) and R_2(y,z) implies R_3(x,z).

Notes:

• originally defined in the KIF-RELATIONS ontology

Axioms for Composition:

(Nth-Domain@Frame-Ontology Composition 3 Binary-Relation)

(Nth-Domain@Frame-Ontology Composition 2 Binary-Relation)

(Nth-Domain@Frame-Ontology Composition 1 Binary-Relation)

Implication Axioms mentioning Composition:

(=> (Composition-Of@Frame-Ontology ?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@Frame-Ontology 
                     ?Left-Sub-Relation
                     (Butlast ?List-Of-Relations))))))

Equivalence Axioms mentioning Composition:

(<=> (Composition-Of@Frame-Ontology ?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@Frame-Ontology 
                           ?Left-Sub-Relation
                           (Butlast ?List-Of-Relations)))))))