Class Empty

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

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

Arity@Frame-Ontology: 1

Documentation@Ol%Frame-Ontology:

True of the empty set.

Notes:

• Source: KIF Version 3.0 Specification

---

Slots:

Equivalence Axioms for Empty:

(<=> (Empty ?X) (= ?X (Setof)))

Implication Axioms mentioning Empty:

(=> (= (Arity@Frame-Ontology ?Relation) ?N) (Not (Empty ?Relation)))

(=> (= (Exact-Domain@Frame-Ontology ?Relation) ?Domain-Relation)
    (Forall (?Tuple)
            (=> (Member ?Tuple ?Relation)
                (Not (Empty (Butlast@Ol-User%Kif-Lists ?Tuple))))))

(=> (Facet@Frame-Ontology ?Relation) (Not (Empty ?Relation)))

(=> (Binary-Function@Ol-User%Kif-Relations ?F) (Not (Empty ?F)))

(=> (Unary-Relation@Ol-User%Kif-Relations ?Relation)
    (Not (Empty ?Relation)))

Equivalence Axioms mentioning Empty:

(<=> (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))

(<=> (Mutually-Disjoint @Sets) (Empty (Intersection @Sets)))

(<=> (Arity@Frame-Ontology ?Relation)
     (And (Relation@Ol-User%Kif-Relations ?Relation)
          (Not (Empty ?Relation))
          (Integer@Ol-User%Kif-Numbers ?N)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (= (Length@Ol-User%Kif-Lists ?Tuple) ?N)))))

(<=> (Exact-Domain@Frame-Ontology ?Relation)
     (And (Relation@Ol-User%Kif-Relations ?Relation)
          (Relation@Ol-User%Kif-Relations ?Domain-Relation)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (Not (Empty (Butlast@Ol-User%Kif-Lists ?Tuple)))))
          (Forall (?Tuple @Args)
                  (<=> (Holds@Ol-User%Kif-Relations ?Domain-Relation
                              @Args)
                       (And (Member ?Tuple ?Relation)
                            (= (Listof @Args)
                               (Butlast@Ol-User%Kif-Lists ?Tuple)))))))

(<=> (Facet@Frame-Ontology ?Relation)
     (And (Relation@Ol-User%Kif-Relations ?Relation)
          (Not (Empty ?Relation))
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (Triple@Ol-User%Kif-Lists ?Tuple)))))

Axioms mentioning Empty:

(Forall (?S)
        (=> (Not (Empty ?S))
            (Exists (?U) (And (Member ?U ?S) (Disjoint ?U ?S)))))

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

(Exists (?U)
        (And (Bounded ?U)
             (Not (Empty ?U))
             (Forall (?X)
                     (=> (Member ?X ?U)
                         (Exists (?Y)
                                 (And (Member ?Y ?U)
                                      (Proper-Subset ?X ?Y)))))))