Class SET

• Defined in theory: Kif-sets
• Source code: kif-sets.lisp

Slots on this class:

Documentation:

A set is a collection of objects, both individuals and sets of various sorts. It is a KIF primitive.

Instance-Of: Class

Domain-Of:

Complement, Generalized-intersection, Generalized-union, Subset

Range-Of:

Complement, Generalized-intersection, Generalized-union, Intersection, Member, Subset, Union

Superclass-Of: Proper-set, Simple-set

Other Related Axioms:

(Instance-Of (Set ?X) Not)

(Not (Set ?X))

(<=> (Individual ?X) (Not (Set ?X)))

(<=> (Simple-Set ?X) (And (Set ?X) (Bounded ?X)))

(=> (Member $X $Y) (Set $Y))

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

(=> (Union $X $Y) (Set $Y))

(=> (= (Union @Sets) ?Set) (=> (Item ?S (Listof @Sets)) (Set ?S)))

(=> (Intersection $X $Y) (Set $Y))

(=> (= (Intersection @Sets) ?Set)
    (=> (Item ?S (Listof @Sets)) (Set ?S)))

(Nth-Domain Difference 3 Set)

(Nth-Domain Difference 1 Set)

(=> (= (Difference ?Set @Sets) ?Diff-Set)
    (=> (Item ?S (Listof @Sets)) (Set ?S)))

(=> (Complement $X $Y) (Set $Y))

(=> (Complement $X $Y) (Set $X))

(=> (Generalized-Union $X $Y) (Set $Y))

(=> (Generalized-Union $X $Y) (Set $X))

(=> (Generalized-Intersection $X $Y) (Set $Y))

(=> (Generalized-Intersection $X $Y) (Set $X))

(=> (Subset $X $Y) (Set $Y))

(=> (Subset $X $Y) (Set $X))

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

(Exists (?S)
        (And (Set ?S)
             (Forall (?X) (=> (Member ?X ?S) (Double ?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)))))))

(=> (And (Bounded ?U) (Set ?S)) (Bounded (Intersection ?U ?S)))

Notes:

• Source: KIF Version 3.0 Specification