Relation Member

• 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: Binary-Relation@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set

Domain@Frame-Ontology: Bounded

Range@Frame-Ontology: Set

Arity@Frame-Ontology: 2

Documentation@Ol%Frame-Ontology:

The sentence {tt (member $tau_1$ $tau_2$)} is true if and only if the object denoted by $tau_1$ is contained in the set denoted by $tau_2$. As mentioned above, an object can be a member of another object if and only if the former is bounded and the latter is a set.

Notes:

• Source: KIF Version 3.0 Specification

Implication Axioms mentioning Member:

(=> (= (Generalized-Union ?Set-Of-Sets) ?Set)
    (Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Simple-Set ?S))))

(=> (= (Generalized-Intersection ?Set-Of-Sets) ?Set)
    (Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Simple-Set ?S))))

(=> (And (Set ?S1) (Set ?S2))
    (<=> (Forall (?X) (<=> (Member ?X ?S1) (Member ?X ?S2)))
         (= ?S1 ?S2)))

(=> (Subset ?S1 ?S2)
    (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2))))

(=> (And (Bounded ?U) (Forall (?X) (=> (Member ?X ?U) (Bounded ?X))))
    (Bounded (Generalized-Union ?U)))

Equivalence Axioms mentioning Member:

(<=> (Subset ?S1 ?S2)
     (And (Set ?S1)
          (Set ?S2)
          (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2)))))

(<=> (Instance-Of@Frame-Ontology ?Individual ?Class)
     (Member (Listof ?Individual) ?Class))

(<=> (All-Instances@Frame-Ontology ?Class)
     (And (Class@Frame-Ontology ?Class)
          (Set ?Set-Of-Instances)
          (Forall (?Instance)
                  (<=> (Member ?Instance ?Set-Of-Instances)
                       (Instance-Of@Frame-Ontology ?Instance ?Class)))))

(<=> (One-Of@Frame-Ontology @Members)
     (Forall (?Instance)
             (<=> (Instance-Of@Frame-Ontology ?Instance ?Class)
                  (Member ?Instance (Setof @Members)))))

(<=> (Subrelation-Of@Frame-Ontology ?Child-Relation ?Parent-Relation)
     (And (Relation@Ol-User%Kif-Relations ?Child-Relation)
          (Relation@Ol-User%Kif-Relations ?Parent-Relation)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Child-Relation)
                      (Member ?Tuple ?Parent-Relation)))))

Axioms mentioning Member:

(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)))))))

(Forall (?Class)
        (=> (Member ?Class ?Set-Of-Classes)
            (Class@Frame-Ontology ?Class)))