 SUMO   View all facts   Glossary   Help Entity > Abstract > Quantity > Number > RealNumber > RationalNumber > Integer
UpRationalNumber  Integer subject fact
 Integer documentation A negative or nonnegative whole number has axiom `(=> (instance ?SEQ SequenceFunction) (subclass (RangeFn ?SEQ) Integer))` has axiom `(=> (and (instance ?INT1 Integer) (instance ?INT2 Integer)) (not (and (lessThan ?INT1 ?INT2) (lessThan ?INT2 (SuccessorFn ?INT1)))))` has axiom `(=> (and (instance ?INT1 Integer) (instance ?INT2 Integer)) (not (and (lessThan ?INT2 ?INT1) (lessThan (PredecessorFn ?INT1) ?INT2))))` has axiom `(=> (equal (CeilingFn ?NUMBER) ?INT) (not (exists (?OTHERINT) (and (instance ?OTHERINT Integer) (greaterThanOrEqualTo ?OTHERINT ?NUMBER) (lessThan ?OTHERINT ?INT)))))` has axiom `(=> (equal (FloorFn ?NUMBER) ?INT) (not (exists (?OTHERINT) (and (instance ?OTHERINT Integer) (lessThanOrEqualTo ?OTHERINT ?NUMBER) (greaterThan ?OTHERINT ?INT)))))` has axiom `(=> (instance ?INT Integer) (equal ?INT (SuccessorFn (PredecessorFn ?INT))))` has axiom `(=> (instance ?INT Integer) (equal ?INT (PredecessorFn (SuccessorFn ?INT))))` has axiom `(=> (instance ?INT Integer) (greaterThan ?INT (PredecessorFn ?INT)))` has axiom `(=> (instance ?INT Integer) (lessThan ?INT (SuccessorFn ?INT)))` has axiom `(=> (instance ?NUMBER RationalNumber) (exists (?INT1 ?INT2) (and (instance ?INT1 Integer) (instance ?INT2 Integer) (equal ?NUMBER (DivisionFn ?INT1 ?INT2)))))` is first domain of PredecessorFn is first domain of SuccessorFn is first domain of YearFn is second domain of ExponentiationFn is second domain of singleValued is partitioned into NegativeInteger, NonnegativeInteger is partitioned into OddInteger, EvenInteger is a kind of RationalNumber Abstract is disjoint from Physical Kinds of Integer :

• EvenInteger (3 facts) - An Integer that is evenly divisible by 2
• NegativeInteger (4 facts) - An Integer that is less than zero
• NonnegativeInteger (1 kind, 15 facts) - An Integer that is greater than or equal to zero
• OddInteger (3 facts) - An Integer that is not evenly divisible by 2
• PrimeNumber (3 facts) - An Integer that is evenly divisible only by itself and 1