| Integer(integer) | | 0, 1, 10, 100, 1000, 101, 105, 11, 110, 115, 12, 120, 125, 13, 130, 135, 14, 140, 145, 15, 150, 155, 16, 160, 165, 17, 170, 175, 18, 180, 19, 190, 2, 20, 200, 21, 22, 23, 24, 25, 26, 27, 28, 29, 3, 30, 300, 31, 32, 33... |
| appearance as argument number 1 |
|
|
| (subclass Integer RationalNumber) | Merge.kif 1989-1989 | Integer is a subclass of rational number |
| (partition Integer OddInteger EvenInteger) | Merge.kif 1990-1990 | Integer is exhaustively partitioned into odd integer and even integer |
| (partition Integer NegativeInteger NonnegativeInteger) | Merge.kif 1991-1991 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
| (documentation Integer EnglishLanguage "A negative or nonnegative whole number.") | Merge.kif 1993-1993 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| (=> (instance ?NUMBER Integer) (equal (ReciprocalFn ?NUMBER) (ExponentiationFn ?NUMBER -1))) |
Merge.kif 5134-5136 | If X is an instance of integer, then equal the reciprocal of X and X raised to the power -1 |
| (=> (and (instance ?NUMBER Integer) (not (equal ?NUMBER 0))) (equal 1 (MultiplicationFn ?NUMBER (ReciprocalFn ?NUMBER)))) |
Merge.kif 5138-5143 | If X is an instance of integer and equal X and 0, then equal 1, X, and the reciprocal of X |
| (=> (instance ?INT Integer) (lessThan ?INT (SuccessorFn ?INT))) |
Merge.kif 5363-5365 | If X is an instance of integer, then X is less than (X+1) |
| (=> (instance ?INT Integer) (equal ?INT (SuccessorFn (PredecessorFn ?INT)))) |
Merge.kif 5376-5378 | If X is an instance of integer, then equal X and ((X+2)+1) |
| (=> (instance ?INT Integer) (equal ?INT (PredecessorFn (SuccessorFn ?INT)))) |
Merge.kif 5380-5382 | If X is an instance of integer, then equal X and ((X+1)+2) |
| (=> (instance ?INT Integer) (greaterThan ?INT (PredecessorFn ?INT))) |
Merge.kif 5396-5398 | If X is an instance of integer, then X is greater than (X+2) |
| (=> (and (shortage ?A ?O ?C ?T ?N) (instance ?N Integer)) (desires ?A (exists (?G) (and (instance ?G Collection) (memberType ?G ?O) (memberCount ?G ?N) (possesses ?A ?G))))) |
Mid-level-ontology.kif 33580-33590 | If there is a shortage of X of Y for Z at W during V and X is an instance of integer, then Z desires there exists U such that U is an instance of collection, Y is a member type of U, X is a member count of U, and Z possesses U |
| (=> (and (shortage ?A ?O ?C ?T ?N) (instance ?N Integer)) (not (exists (?B ?G) (and (instance ?B Buying) (during (WhenFn ?B) ?T) (objectTransferred ?B ?G) (transactionAmount ?B ?C) (agent ?B ?A) (instance ?G Collection) (memberType ?G ?O) (memberCount ?G ?N) (possesses ?A ?G))))) |
Mid-level-ontology.kif 33605-33620 | If there is a shortage of X of Y for Z at W during V and X is an instance of integer, then All of the following hold: (1) there don't exist U (2) T such that U is an instance of buying (3) the time of existence of U takes place during V (4) the object transferred in U is T (5) W is a transaction amount of U (6) Z is an agent of U (7) T is an instance of collection (8) Y is a member type of T (9) X is a member count of T (10) Z possesses T |
| (=> (and (shortage ?A ?O ?C ?T ?N) (instance ?N Integer)) (desires ?A (exists (?B ?G) (and (instance ?B Buying) (during (WhenFn ?B) ?T) (objectTransferred ?B ?G) (transactionAmount ?B ?C) (agent ?B ?A) (instance ?G Collection) (memberType ?G ?O) (memberCount ?G ?N) (possesses ?A ?G))))) |
Mid-level-ontology.kif 33638-33653 | If there is a shortage of X of Y for Z at W during V and X is an instance of integer, then All of the following hold: (1) Z desires there exist U (2) T such that U is an instance of buying (3) the time of existence of U takes place during V (4) the object transferred in U is T (5) W is a transaction amount of U (6) Z is an agent of U (7) T is an instance of collection (8) Y is a member type of T (9) X is a member count of T (10) Z possesses T |
| consequent |
|
|
| (=> (and (instance ?MIT BarMitzvah) (patient ?MIT ?X) (instance ?X Boy) (member ?X ?GROUP) (instance ?GROUP Judaism) (birthdate ?X ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?Y13 ?BD13) (and (instance ?Y13 Integer) (equal ?Y13 (AdditionFn ?Y 13)) (instance ?BD13 (DayFn ?D (MonthFn ?M (YearFn ?Y13)))) (equal (WhenFn ?MIT) (ImmediateFutureFn ?BD13))))) |
Biography.kif 71-87 | If All of the following hold: (1) X is an instance of bar mitzvah (2) Y is a patient of X (3) Y is an instance of boy (4) Y is a member of Z (5) Z is an instance of judaism (6) W is a birthdate of Y (7) W is an instance of the day V of month the month U, then there exist T and S such that T is an instance of integer and equal T and (R and 13) and S is an instance of the day V of month the month U and equal the time of existence of X and immediately after S |
| (=> (and (instance ?MIT BatMitzvah) (patient ?MIT ?X) (instance ?X Girl) (member ?X ?GROUP) (instance ?GROUP Judaism) (birthdate ?X ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?Y13 ?BD13) (and (instance ?Y13 Integer) (equal ?Y13 (AdditionFn ?Y 13)) (instance ?BD13 (DayFn ?D (MonthFn ?M (YearFn ?Y13)))) (equal (WhenFn ?MIT) (ImmediateFutureFn ?BD13))))) |
Biography.kif 102-118 | If All of the following hold: (1) X is an instance of bat mitzvah (2) Y is a patient of X (3) Y is an instance of girl (4) Y is a member of Z (5) Z is an instance of judaism (6) W is a birthdate of Y (7) W is an instance of the day V of month the month U, then there exist T and S such that T is an instance of integer and equal T and (R and 13) and S is an instance of the day V of month the month U and equal the time of existence of X and immediately after S |
| (=> (and (instance ?SEQ SequenceFunction) (range ?SEQ ?CLASS)) (subclass ?CLASS Integer)) |
Merge.kif 3431-3435 | If X is an instance of sequence function and the range of X is an instance of Y, then Y is a subclass of integer |
| (=> (multiplicativeFactor ?N1 ?N2) (exists (?I) (and (instance ?I Integer) (equal ?N2 (MultiplicationFn ?N1 ?I))))) |
Merge.kif 4951-4956 | If X is a multiplicative factor of Y, then there exists Z such that Z is an instance of integer, equal X, Y, and Z |
| (=> (and (instance ?WED Wedding) (date ?WED ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?CLASS ?FUTURE) (and (weddingAnniversary ?WED ?CLASS) (subclass ?CLASS Day) (instance ?FUTURE Integer) (equal ?CLASS (DayFn ?D (MonthFn ?M (YearFn ?FUTURE)))) (greaterThan ?FUTURE ?Y)))) |
Mid-level-ontology.kif 26561-26572 | If X is an instance of wedding, date of X is Y, and Y is an instance of the day Z of month the month W, then All of the following hold: (1) there exist V (2) U such that wedding anniversary X (3) V (4) V is a subclass of day (5) U is an instance of integer (6) equal V (7) the day Z of month the month W (8) U is greater than T |
| (=> (and (birthdate ?A ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?CLASS ?FUTURE) (and (birthday ?A ?CLASS) (subclass ?CLASS Day) (instance ?FUTURE Integer) (equal ?CLASS (DayFn ?D (MonthFn ?M (YearFn ?FUTURE)))) (greaterThan ?FUTURE ?Y)))) |
Mid-level-ontology.kif 26602-26612 | If X is a birthdate of Y and X is an instance of the day Z of month the month W, then All of the following hold: (1) there exist V (2) U such that Y's birthday is V (3) V is a subclass of day (4) U is an instance of integer (5) equal V (6) the day Z of month the month W (7) U is greater than T |
|
|
|