Class Set

Superclass-Of@Frame-Ontology:
Proper-Set, Simple-Set, Class-Partition@Frame-Ontology, Finite-Set@Ol-User%Kif-Extensions, Relation@Ol-User%Kif-Relations ...
Has-Instance@Frame-Ontology:
<@Ol-User%Kif-Numbers, =<@Ol-User%Kif-Numbers, >=@Ol-User%Kif-Numbers, >@Ol-User%Kif-Numbers, After=@Simple-Time, After@Simple-Time, Alias@Frame-Ontology, Before=@Simple-Time, Before@Simple-Time, Can-Be-One-Of@Ol-User%Slot-Constraint-Sugar, Can-Have-One@Ol-User%Slot-Constraint-Sugar, Cannot-Have@Ol-User%Slot-Constraint-Sugar, Composition-Of@Frame-Ontology, Defining-Axiom@Ol-User%Kif-Meta, Direct-Instance-Of@Frame-Ontology, Direct-Subclass-Of@Frame-Ontology, Disjoint, Disjoint-Time-Ranges@Simple-Time, Documentation@Ol%Frame-Ontology, Domain-Of@Frame-Ontology, Domain@Frame-Ontology, During=@Simple-Time, During@Simple-Time, Equals@Simple-Time, Exhaustive-Subclass-Partition@Frame-Ontology, Finishes=@Simple-Time, Finishes@Simple-Time, Has-At-Least@Ol-User%Slot-Constraint-Sugar, Has-At-Most@Ol-User%Slot-Constraint-Sugar, Has-Instance@Frame-Ontology, Has-Name@Agents, Has-One-Of-Type@Ol-User%Slot-Constraint-Sugar, Has-One@Ol-User%Slot-Constraint-Sugar, Has-Single-Slot-Value-Of-Type@Ol-User%Slot-Constraint-Sugar, Has-Slot-Value-Of-Type@Ol-User%Slot-Constraint-Sugar, Has-Slot-Value@Ol-User%Slot-Constraint-Sugar, Has-Some@Ol-User%Slot-Constraint-Sugar, Has-Subdefinition@Frame-Ontology, Has-Subrelation@Frame-Ontology, Has-Value-Of-Type@Ol-User%Slot-Constraint-Sugar, Has-Value@Frame-Ontology, Has-Values@Ol-User%Slot-Constraint-Sugar, Holds@Ol-User%Kif-Relations, Inherited-Facet-Value@Frame-Ontology, Inherited-Slot-Value@Frame-Ontology, Instance-Of@Frame-Ontology, Item@Ol-User%Kif-Lists, Logbit@Ol-User%Kif-Numbers, Logtest@Ol-User%Kif-Numbers, Maximum-Slot-Cardinality@Frame-Ontology, Maximum-Value-Cardinality@Frame-Ontology, Meets@Simple-Time, Member, Minimum-Slot-Cardinality@Frame-Ontology, Minimum-Value-Cardinality@Frame-Ontology, Must-Be-One-Of@Ol-User%Slot-Constraint-Sugar, Mutually-Disjoint, Nth-Domain@Frame-Ontology, Onto@Frame-Ontology, Overlaps=@Simple-Time, Overlaps@Simple-Time, Pairwise-Disjoint, Picture@Interface-Ontology, Proper-Subset, Range-Of@Frame-Ontology, Range@Frame-Ontology, Related-Axioms@Frame-Ontology, Same-Slot-Values@Frame-Ontology, Same-Values@Frame-Ontology, Set-Cover, Set-Partition, Single-Valued-Slot@Frame-Ontology, Slot-Documentation@Frame-Ontology, Slot-Value-Type@Frame-Ontology, Start=@Simple-Time, Starts@Simple-Time, Subclass-Of@Frame-Ontology, Subclass-Partition@Frame-Ontology, Sublist@Ol-User%Kif-Lists, Subrelation-Of@Frame-Ontology, Subset, Superclass-Of@Frame-Ontology, Total-On@Frame-Ontology, Value-Type@Frame-Ontology, Visible-Slots-For-Query@Interface-Ontology
Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation@Ol-User%Kif-Relations, Set
Domain-Of@Frame-Ontology:
Complement, Generalized-Intersection, Generalized-Union, Subset, Cardinality@Ol-User%Kif-Extensions ...
Range-Of@Frame-Ontology:
Complement, Generalized-Intersection, Generalized-Union, Subset, All-Instances@Frame-Ontology ...
Arity@Frame-Ontology: 1
Documentation@Ol%Frame-Ontology:
A set is a collection of objects, both individuals and sets of various sorts. It is a KIF primitive.

Notes:

Slots:

Cardinality@Ol-User%Kif-Extensions:
Generalized-Intersection:
Generalized-Union:

Implication Axioms mentioning Set:

(=> (Union @Sets ?Set) (Set ?Set))

(=> (Intersection @Sets ?Set) (Set ?Set))

(=> (= (Union @Sets) ?Set)
    (=> (Item@Ol-User%Kif-Lists ?S (Listof @Sets)) (Set ?S)))

(=> (= (Intersection @Sets) ?Set)
    (=> (Item@Ol-User%Kif-Lists ?S (Listof @Sets)) (Set ?S)))

(=> (= (Difference ?Set @Sets) ?Diff-Set)
    (=> (Item@Ol-User%Kif-Lists ?S (Listof @Sets)) (Set ?S)))

Equivalence Axioms mentioning Set:

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

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

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

(<=> (Cardinality@Ol-User%Kif-Extensions ?Set)
     (And (Set ?Set)
          (Exists (@Elements)
                  (And (= ?Set (Setof @Elements))
                       (= ?Integer
                          (Length@Ol-User%Kif-Lists (Listof @Elements)))))))

(<=> (Finite-Set@Ol-User%Kif-Extensions ?F-Set)
     (And (Set ?F-Set)
          (Exists (@Elements) (= ?F-Set (Setof @Elements)))))

Axioms mentioning Set:

(Nth-Domain@Frame-Ontology Difference 3 Set)

(Nth-Domain@Frame-Ontology Difference 1 Set)

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

(Nth-Domain@Frame-Ontology Has-Values@Ol-User%Slot-Constraint-Sugar
            3
            Set)