SUMO   View all facts   Glossary   Help
Entity > Abstract > Quantity > Number > RealNumber > RationalNumber > Integer
Up: RationalNumber

Integer
subjectfact 
Integerdocumentation A negative or nonnegative whole number2001-11-30 13:34:30.0
has axiom 
(=> 
    (instance ?SEQ SequenceFunction) 
    (subclass (RangeFn ?SEQ)  Integer))
2001-11-30 13:34:31.0
has axiom 
(=>
    (and
       (instance ?INT1 Integer)
       (instance ?INT2 Integer))
    (not
       (and
          (lessThan ?INT1 ?INT2)
          (lessThan ?INT2 (SuccessorFn ?INT1)))))
2001-11-30 13:34:31.0
has axiom 
(=>
    (and
       (instance ?INT1 Integer)
       (instance ?INT2 Integer))
    (not
       (and
          (lessThan ?INT2 ?INT1)
          (lessThan (PredecessorFn ?INT1) ?INT2))))
2001-11-30 13:34:31.0
has axiom 
(=>
    (equal (CeilingFn ?NUMBER) ?INT)
    (not
       (exists (?OTHERINT)
          (and
             (instance ?OTHERINT Integer)
             (greaterThanOrEqualTo ?OTHERINT ?NUMBER)
             (lessThan ?OTHERINT ?INT)))))
2001-11-30 13:34:31.0
has axiom 
(=>
    (equal (FloorFn ?NUMBER) ?INT)
    (not
       (exists (?OTHERINT)
          (and
             (instance ?OTHERINT Integer)
             (lessThanOrEqualTo ?OTHERINT ?NUMBER)
             (greaterThan ?OTHERINT ?INT)))))
2001-11-30 13:34:31.0
has axiom 
(=>
    (instance ?INT Integer)
    (equal ?INT (SuccessorFn (PredecessorFn ?INT))))
2001-11-30 13:34:31.0
has axiom 
(=>
    (instance ?INT Integer)
    (equal ?INT (PredecessorFn (SuccessorFn ?INT))))
2001-11-30 13:34:31.0
has axiom 
(=>
    (instance ?INT Integer)
    (greaterThan ?INT (PredecessorFn ?INT)))
2001-11-30 13:34:31.0
has axiom 
(=>
    (instance ?INT Integer)
    (lessThan ?INT (SuccessorFn ?INT)))
2001-11-30 13:34:31.0
has axiom 
(=>
    (instance ?NUMBER RationalNumber)
    (exists (?INT1 ?INT2)
       (and
          (instance ?INT1 Integer)
          (instance ?INT2 Integer)
          (equal ?NUMBER (DivisionFn ?INT1 ?INT2)))))
2001-11-30 13:34:31.0
is first domain of PredecessorFn2001-11-30 13:34:31.0
is first domain of SuccessorFn2001-11-30 13:34:31.0
is first domain of YearFn2001-11-30 13:34:31.0
is second domain of ExponentiationFn2001-11-30 13:34:31.0
is second domain of singleValued2001-11-30 13:34:31.0
is partitioned into NegativeInteger, NonnegativeInteger2001-11-30 13:34:31.0
is partitioned into OddInteger, EvenInteger2001-11-30 13:34:31.0
is a kind of RationalNumber2001-11-30 13:34:31.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Kinds of Integer :

Up: RationalNumber