InsiemeOClasse (SetOrClass)

The SetOrClass of Sets and Classes, i.e. any instance of Abstract that has elements or instances.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

Entitá

Astratto

InsiemeOClasse

Subclass(es)

Classe Insieme ClasseDisgiuntaACoppie ClasseMutualmenteDisgiunta

Coordinate term(s)

Attributo Grafo ElementoDelGrafo Proposizione Quantitá Relazione

Constrains relations

cardinality fn complement fn generalized intersection fn generalized union fn intersection fn kappa fn power set fn relative complement fn union fn closed on disjoint domain domain subclass equivalence relation on instance irreflexive on partial ordering on range range subclass reflexive on subclass total ordering on trichotomizing on

Axioms (4)

subclass é una sottoclasse di class se e solo se

subclass é un' istanza di InsiemeOClasse
class é un' istanza di InsiemeOClasse
per ogni inst vale: se inst é un' istanza di subclass, allora inst é un' istanza di class

(<=>
      (subclass ?SUBCLASS ?CLASS)
      (and
            (instance ?SUBCLASS SetOrClass)
            (instance ?CLASS SetOrClass)
            (forall
                  (?INST)
                  (=>
                        (instance ?INST ?SUBCLASS)
                        (instance ?INST ?CLASS)))))

class1 é disgiunto da class2 se e solo se

class1 é un' istanza di InsiemeOClasse
class2 é un' istanza di InsiemeOClasse
per ogni inst vale: inst é not un' istanza di class1 o inst é not un' istanza di class2

(<=>
      (disjoint ?CLASS1 ?CLASS2)
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass)
            (forall
                  (?INST)
                  (not
                        (and
                              (instance ?INST ?CLASS1)
                              (instance ?INST ?CLASS2))))))

InsiemeOClasse é esaustivamente partizionato in Insieme,Classe.

(partition SetOrClass Set Class)

Se class1 é un' istanza di InsiemeOClasse e class2 é un' istanza di InsiemeOClasse, allora "la differenza tra class1 e class2" is uguale a "l' unione di class1 e "il complemento di class2"".

(=>
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass))
      (equal
            (RelativeComplementFn ?CLASS1 ?CLASS2)
            (IntersectionFn
                  ?CLASS1
                  (ComplementFn ?CLASS2))))