Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| 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 |
|
|
| s__subclass(s__Integer,s__RationalNumber)
|
Merge.kif 2058-2058 | Integer is a subclass of rational number |
| s__partition(s__Integer,s__OddInteger,s__EvenInteger)
|
Merge.kif 2059-2059 | Integer is exhaustively partitioned into odd integer and even integer |
| s__partition(s__Integer,s__NegativeInteger,s__NonnegativeInteger)
|
Merge.kif 2060-2060 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
| s__documentation(s__Integer, s__EnglishLanguage, "A negative or nonnegative whole number_") | Merge.kif 2062-2062 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| ! [V__NUMBER] : ((s__instance(V__NUMBER,s__Integer) => (s__ReciprocalFn(V__NUMBER) = s__ExponentiationFn(V__NUMBER,n___1))) )
|
Merge.kif 5194-5196 | If X is an instance of integer, then equal the reciprocal of X and X raised to the power -1 |
| ! [V__NUMBER] : (((s__instance(V__NUMBER,s__Integer) & ~((V__NUMBER = n__0))) => (n__1 = s__MultiplicationFn(V__NUMBER,s__ReciprocalFn(V__NUMBER)))) )
|
Merge.kif 5198-5203 | If X is an instance of integer and equal X and 0, then equal 1, X, and the reciprocal of X |
| ! [V__INT] : ((s__instance(V__INT,s__Integer) => s__lessThan(V__INT,s__SuccessorFn(V__INT))) )
|
Merge.kif 5434-5436 | If X is an instance of integer, then X is less than (X+1) |
| ! [V__INT] : ((s__instance(V__INT,s__Integer) => (V__INT = s__SuccessorFn(s__PredecessorFn(V__INT)))) )
|
Merge.kif 5447-5449 | If X is an instance of integer, then equal X and ((X+2)+1) |
| ! [V__INT] : ((s__instance(V__INT,s__Integer) => (V__INT = s__PredecessorFn(s__SuccessorFn(V__INT)))) )
|
Merge.kif 5451-5453 | If X is an instance of integer, then equal X and ((X+1)+2) |
| ! [V__INT] : ((s__instance(V__INT,s__Integer) => s__greaterThan(V__INT,s__PredecessorFn(V__INT))) )
|
Merge.kif 5467-5469 | If X is an instance of integer, then X is greater than (X+2) |
| ! [V__A : $i,V__C : $i,V__N : $int,V__O : $i,V__T : $i] : ((s__shortage(V__A, V__O, V__C, V__T, V__N) => s__desires(V__A, ( ? [V__G:$i] : ((s__instance(V__G, s__CollectionOfObjects) & s__memberType(V__G, V__O) & s__memberCount(V__G, V__N) & s__possesses(V__A, V__G))))))) | Mid-level-ontology.kif 33506-33516 | 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 |
| ! [V__A,V__O,V__C,V__T,V__N] : (((s__instance(V__A,s__AutonomousAgent) & s__instance(V__O,s__Class) & s__subclass(V__O,s__Object) & s__instance(V__C,s__CurrencyMeasure) & s__instance(V__T,s__TimeInterval)) => ((s__shortage(V__A,V__O,V__C,V__T,V__N) & s__instance(V__N,s__Integer)) => ~((? [V__B,V__G] : ((s__instance(V__B,s__Buying) & s__during(s__WhenFn(V__B) ,V__T) & s__objectTransferred(V__B,V__G) & s__transactionAmount(V__B,V__C) & s__agent(V__B,V__A) & s__instance(V__G,s__CollectionOfObjects) & s__memberType(V__G,V__O) & s__memberCount(V__G,V__N) & s__possesses(V__A,V__G))))))) )
|
Mid-level-ontology.kif 33531-33546 | 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 |
| ! [V__A : $i,V__C : $i,V__N : $int,V__O : $i,V__T : $i] : ((s__shortage(V__A, V__O, V__C, V__T, V__N) => s__desires(V__A, ( ? [V__B:$i, V__G:$i] : ((s__instance(V__B, s__Buying) & s__during(s__WhenFn(V__B), V__T) & s__objectTransferred(V__B, V__G) & s__transactionAmount(V__B, V__C) & s__agent(V__B, V__A) & s__instance(V__G, s__CollectionOfObjects) & s__memberType(V__G, V__O) & s__memberCount(V__G, V__N) & s__possesses(V__A, V__G))))))) | Mid-level-ontology.kif 33564-33579 | 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 |
|
|
| ! [V__CLASS,V__SEQ] : ((s__instance(V__CLASS,s__Class) => ((s__instance(V__SEQ,s__SequenceFunction) & s__range(V__SEQ,V__CLASS)) => s__subclass(V__CLASS,s__Integer))) )
|
Merge.kif 3505-3509 | 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 |
| ! [V__N1,V__N2] : (((s__instance(V__N1,s__Integer) & s__instance(V__N2,s__Integer)) => (s__multiplicativeFactor(V__N1,V__N2) => (? [V__I] : ((s__instance(V__I,s__Integer) & (V__N2 = s__MultiplicationFn(V__N1,V__I))))))) )
|
Merge.kif 5011-5016 | 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 |
| ! [V__DAY,V__D,V__M,V__Y,V__WED] : (((s__instance(V__DAY,s__Day) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer)) => ((s__instance(V__WED,s__Wedding) & s__date(V__WED,V__DAY) & s__instance(V__DAY,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) => (? [V__CLASS,V__FUTURE] : ((s__instance(V__CLASS,s__Class) & s__subclass(V__CLASS,s__Day) & (s__weddingAnniversary(V__WED,V__CLASS) & s__subclass(V__CLASS,s__Day) & s__instance(V__FUTURE,s__Integer) & (V__CLASS = s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__FUTURE)))) & s__greaterThan(V__FUTURE,V__Y))))))) )
|
Mid-level-ontology.kif 26479-26490 | 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 |
| ! [V__A,V__DAY,V__D,V__M,V__Y] : (((s__instance(V__A,s__Human) & s__instance(V__DAY,s__Day) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer)) => ((s__birthdate(V__A,V__DAY) & s__instance(V__DAY,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) => (? [V__CLASS,V__FUTURE] : ((s__instance(V__CLASS,s__Class) & s__subclass(V__CLASS,s__Day) & (s__birthday(V__A,V__CLASS) & s__subclass(V__CLASS,s__Day) & s__instance(V__FUTURE,s__Integer) & (V__CLASS = s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__FUTURE)))) & s__greaterThan(V__FUTURE,V__Y))))))) )
|
Mid-level-ontology.kif 26520-26530 | 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 |
| ! [V__DAY,V__D,V__M,V__Y,V__MIT,V__X,V__GROUP] : (((s__instance(V__DAY,s__Day) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer)) => ((s__instance(V__MIT,s__BarMitzvah) & s__patient(V__MIT,V__X) & s__instance(V__X,s__Boy) & s__member(V__X,V__GROUP) & s__instance(V__GROUP,s__Judaism) & s__birthdate(V__X,V__DAY) & s__instance(V__DAY,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) => (? [V__Y13,V__BD13] : ((s__instance(V__BD13,s__TimePosition) & (s__instance(V__Y13,s__Integer) & (V__Y13 = s__AdditionFn(V__Y,n__13)) & s__instance(V__BD13,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y13)))) & (s__WhenFn(V__MIT) = s__ImmediateFutureFn(V__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 |
| ! [V__DAY,V__D,V__M,V__Y,V__MIT,V__X,V__GROUP] : (((s__instance(V__DAY,s__Day) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer)) => ((s__instance(V__MIT,s__BatMitzvah) & s__patient(V__MIT,V__X) & s__instance(V__X,s__Girl) & s__member(V__X,V__GROUP) & s__instance(V__GROUP,s__Judaism) & s__birthdate(V__X,V__DAY) & s__instance(V__DAY,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) => (? [V__Y13,V__BD13] : ((s__instance(V__BD13,s__TimePosition) & (s__instance(V__Y13,s__Integer) & (V__Y13 = s__AdditionFn(V__Y,n__13)) & s__instance(V__BD13,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y13)))) & (s__WhenFn(V__MIT) = s__ImmediateFutureFn(V__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 |
|