Class BOUNDED

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

Slots on this class:

Documentation:

Something is bounded if it can be a member of a set. This is a KIF primitive.

Instance-Of: Class

Domain-Of: Member

Superclass-Of: Simple-set

Other Related Axioms:

(Instance-Of (Bounded ?X) Not)

(Not (Bounded ?X))

(<=> (Unbounded ?X) (Not (Bounded ?X)))

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

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

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

(=> (Finite-Set ?S) (Bounded ?S))

(=> (Bounded ?V) (Bounded (Setofall ?U (Subset ?U ?V))))

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

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

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

Notes:

• Source: KIF Version 3.0 Specification