Class Double

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

Subclass-Of@Frame-Ontology: List

Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets

Arity@Frame-Ontology: 1

Documentation@Ol%Frame-Ontology: A list of length 2.

---

Slots:

Equivalence Axioms for Double:

(<=> (Double ?List) (And (List ?List) (= (Length ?List) 2)))

Implication Axioms mentioning Double:

(=> (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@Ol-User%Kif-Relations 
                    (First (Rest ?List-Of-Relations))
                    (First ?List-Of-Relations))))
        (Exists 
            (?Left-Sub-Relation)
            (And (= ?Binary-Relation
                    (Composition@Ol-User%Kif-Relations 
                        (Last ?List-Of-Relations)
                        ?Left-Sub-Relation))
                 (Composition-Of@Frame-Ontology 
                     ?Left-Sub-Relation
                     (Butlast ?List-Of-Relations))))))

(=> (Binary-Relation@Ol-User%Kif-Relations ?Relation)
    (Forall (?Tuple)
            (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
                (Double ?Tuple))))

Equivalence Axioms mentioning Double:

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

(<=> (Binary-Relation@Ol-User%Kif-Relations ?Relation)
     (And (Relation@Ol-User%Kif-Relations ?Relation)
          (Not (Empty@Ol-User%Kif-Sets ?Relation))
          (Forall (?Tuple)
                  (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
                      (Double ?Tuple)))))

Axioms mentioning Double:

(Exists (?S)
        (And (Set@Ol-User%Kif-Sets ?S)
             (Forall (?X)
                     (=> (Member@Ol-User%Kif-Sets ?X ?S) (Double ?X)))
             (Forall (?X ?Y ?Z)
                     (=> (And (Member@Ol-User%Kif-Sets (Listof ?X ?Y)
                                      ?S)
                              (Member@Ol-User%Kif-Sets (Listof ?X ?Z)
                                      ?S))
                         (= ?Y ?Z)))
             (Forall (?U)
                     (=> (And (Bounded@Ol-User%Kif-Sets ?U)
                              (Not (Empty@Ol-User%Kif-Sets ?U)))
                         (Exists (?V)
                                 (And (Member@Ol-User%Kif-Sets ?V ?U)
                                      (Member@Ol-User%Kif-Sets 
                                          (Listof ?U ?V)
                                          ?S)))))))