Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| YearFn |
| appearance as argument number 1 |
|
| s__instance(s__YearFn,s__TemporalRelation)
|
Merge.kif 8754-8754 | Year is an instance of temporal relation |
| s__instance(s__YearFn,s__UnaryFunction)
|
Merge.kif 8755-8755 | Year is an instance of unary function |
| s__instance(s__YearFn,s__TotalValuedRelation)
|
Merge.kif 8756-8756 | Year is an instance of total valued relation |
| s__domain(s__YearFn,n__1,s__Integer)
|
Merge.kif 8757-8757 | The number 1 argument of year is an instance of integer |
| s__rangeSubclass(s__YearFn,s__Year)
|
Merge.kif 8758-8758 | The values returned by year are subclasses of year |
| s__documentation(s__YearFn, s__EnglishLanguage, "A UnaryFunction that maps a number to the corresponding calendar Year_ For example, (YearFn 1912) returns the Class containing just one instance, the year of 1912_ As might be expected, positive integers return years in the Common Era, while negative integers return years in B_C_E_ Note that this function returns a Class as a value_ The reason for this is that the related functions, viz_ MonthFn, DayFn, HourFn, MinuteFn, and SecondFn, are used to generate both specific TimeIntervals and recurrent intervals, and the only way to do this is to make the domains and ranges of these functions classes rather than individuals_") | Merge.kif 8760-8768 | The values returned by year are subclasses of year |
| appearance as argument number 2 |
|
|
| s__relatedInternalConcept(s__Year,s__YearFn)
|
Merge.kif 8941-8941 | Year is internally related to year |
| s__termFormat(s__EnglishLanguage, s__YearFn, "year") | domainEnglishFormat.kif 63758-63758 | Year is internally related to year |
| s__termFormat(s__ChineseTraditionalLanguage, s__YearFn, "年") | domainEnglishFormat.kif 63759-63759 | Year is internally related to year |
| s__termFormat(s__ChineseLanguage, s__YearFn, "年") | domainEnglishFormat.kif 63760-63760 | Year is internally related to year |
| s__format(s__EnglishLanguage, s__YearFn, "the year %1") | english_format.kif 471-471 | Year is internally related to year |
| antecedent |
|
|
| ! [V__Y1,V__N1,V__Y2,V__N2,V__T1,V__T2] : (((s__instance(V__Y1,s__TimeInterval) & s__instance(V__N1,s__Integer) & s__instance(V__Y2,s__TimeInterval) & s__instance(V__N2,s__Integer) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => ((s__instance(V__Y1,s__YearFn(V__N1)) & s__instance(V__Y2,s__YearFn(V__N2)) & (V__T1 = s__BeginFn(V__Y1)) & (V__T2 = s__BeginFn(V__Y2)) & s__greaterThan(V__N2,V__N1)) => s__before(V__T1,V__T2))) )
|
Merge.kif 8892-8899 | If X is an instance of the year Y, Z is an instance of the year W, equal V and the beginning of X, equal U and the beginning of Z, and W is greater than Y, then V happens before U |
| ! [V__Y1,V__N1,V__Y2,V__N2] : (((s__instance(V__Y1,s__TimeInterval) & s__instance(V__N1,s__Integer) & s__instance(V__Y2,s__TimeInterval) & s__instance(V__N2,s__Integer)) => ((s__instance(V__Y1,s__YearFn(V__N1)) & s__instance(V__Y2,s__YearFn(V__N2)) & s__greaterThan(V__N2,V__N1)) => s__earlier(V__Y1,V__Y2))) )
|
Merge.kif 8901-8906 | If X is an instance of the year Y, Z is an instance of the year W, and W is greater than Y, then X happens earlier than Z |
| ! [V__M1,V__N1,V__Y,V__M2,V__N2,V__T1,V__T2] : (((s__instance(V__M1,s__TimeInterval) & s__instance(V__N1,s__Class) & s__subclass(V__N1,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__M2,s__TimeInterval) & s__instance(V__N2,s__Class) & s__subclass(V__N2,s__Month) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => ((s__instance(V__M1,s__MonthFn(V__N1,s__YearFn(V__Y))) & s__instance(V__M2,s__MonthFn(V__N2,s__YearFn(V__Y))) & (V__T1 = s__BeginFn(V__M1)) & (V__T2 = s__BeginFn(V__M2)) & s__successorClass(V__N1,V__N2)) => s__before(V__T1,V__T2))) )
|
Merge.kif 8908-8915 | If X is an instance of the month Y, Z is an instance of the month W, equal V and the beginning of X, equal U and the beginning of Z, and W is the successor class of Y., then V happens before U |
| ! [V__M1,V__N1,V__Y,V__M2,V__N2] : (((s__instance(V__M1,s__TimeInterval) & s__instance(V__N1,s__Class) & s__subclass(V__N1,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__M2,s__TimeInterval) & s__instance(V__N2,s__Class) & s__subclass(V__N2,s__Month)) => ((s__instance(V__M1,s__MonthFn(V__N1,s__YearFn(V__Y))) & s__instance(V__M2,s__MonthFn(V__N2,s__YearFn(V__Y))) & s__successorClass(V__N1,V__N2)) => s__earlier(V__M1,V__M2))) )
|
Merge.kif 8917-8922 | If X is an instance of the month Y, Z is an instance of the month W, and W is the successor class of Y., then X happens earlier than Z |
| ! [V__D1,V__N1,V__M,V__Y,V__D2,V__N2,V__T1,V__T2] : (((s__instance(V__D1,s__TimeInterval) & s__instance(V__N1,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__D2,s__TimeInterval) & s__instance(V__N2,s__PositiveInteger) & s__instance(V__T1,s__TimePoint) & s__instance(V__T2,s__TimePoint)) => ((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))) & (V__T1 = s__BeginFn(V__D1)) & (V__T2 = s__BeginFn(V__D2)) & s__greaterThan(V__N2,V__N1)) => s__before(V__T1,V__T2))) )
|
Merge.kif 8924-8931 | If X is an instance of the day Y of month the month Z, W is an instance of the day V of month the month Z, equal U and the beginning of X, equal T and the beginning of W, and V is greater than Y, then U happens before T |
| ! [V__D1,V__N1,V__M,V__Y,V__D2,V__N2] : (((s__instance(V__D1,s__TimeInterval) & s__instance(V__N1,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__D2,s__TimeInterval) & s__instance(V__N2,s__PositiveInteger)) => ((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__greaterThan(V__N2,V__N1)) => s__earlier(V__D1,V__D2))) )
|
Merge.kif 8933-8938 | If X is an instance of the day Y of month the month Z, W is an instance of the day V of month the month Z, and V is greater than Y, then X happens earlier than W |
| ! [V__Y1,V__N1,V__Y2,V__N2] : (((s__instance(V__Y1,s__TimeInterval) & s__instance(V__N1,s__Integer) & s__instance(V__Y2,s__TimeInterval) & s__instance(V__N2,s__Integer)) => ((s__instance(V__Y1,s__YearFn(V__N1)) & s__instance(V__Y2,s__YearFn(V__N2)) & (s__SubtractionFn(V__N2,V__N1) = n__1)) => s__meetsTemporally(V__Y1,V__Y2))) )
|
Merge.kif 8950-8955 | If X is an instance of the year Y, Z is an instance of the year W, and equal (W and Y) and 1, then X meets Z |
| ! [V__N,V__Y,V__YI,V__Q] : (((s__instance(V__N,s__PositiveInteger) & s__instance(V__Y,s__Integer) & s__instance(V__YI,s__TimeInterval)) => ((s__instance(V__Q,s__QuarterYear) & s__instance(V__Q,s__QuarterFn(V__N,s__YearFn(V__Y))) & s__instance(V__YI,s__YearFn(V__Y))) => s__during(V__Q,V__YI))) )
|
Merge.kif 9182-9187 | If X is an instance of quarter year, X is an instance of the number Y quarter of the year Z, and W is an instance of the year Z, then X takes place during W |
| ! [V__NUMBER,V__LEAP] : ((s__instance(V__NUMBER,s__Integer) => ((s__instance(V__LEAP,s__LeapYear) & s__instance(V__LEAP,s__YearFn(V__NUMBER))) => (((s__RemainderFn(V__NUMBER,n__4) = n__0) & ~((s__RemainderFn(V__NUMBER,n__100) = n__0))) | (s__RemainderFn(V__NUMBER,n__400) = n__0)))) )
|
Merge.kif 9203-9211 | If X is an instance of leap year and X is an instance of the year Y, then equal Y mod 4 and 0 and equal Y mod 100 and 0 or equal Y mod 400 and 0 |
| ! [V__UTC,V__H1,V__D,V__M,V__Y,V__PST,V__H2] : (((s__instance(V__UTC,s__TimePosition) & s__instance(V__H1,s__NonnegativeInteger) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__PST,s__TimePosition) & s__instance(V__H2,s__NonnegativeInteger)) => ((s__instance(V__UTC,s__HourFn(V__H1,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & s__instance(V__PST,s__HourFn(V__H2,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & (s__RelativeTimeFn(V__UTC,s__PacificTimeZone) = V__PST)) => (V__H2 = s__AdditionFn(V__H1,n__8)))) )
|
Merge.kif 17532-17538 | If X is an instance of the hour Y, Z is an instance of the hour W, and equal the time X in zone pacific time zone and Z, then equal W and (Y and 8) |
| ! [V__UTC,V__H1,V__D,V__M,V__Y,V__MST,V__H2] : (((s__instance(V__UTC,s__TimePosition) & s__instance(V__H1,s__NonnegativeInteger) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__MST,s__TimePosition) & s__instance(V__H2,s__NonnegativeInteger)) => ((s__instance(V__UTC,s__HourFn(V__H1,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & s__instance(V__MST,s__HourFn(V__H2,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & (s__RelativeTimeFn(V__UTC,s__MountainTimeZone) = V__MST)) => (V__H2 = s__AdditionFn(V__H1,n__7)))) )
|
Merge.kif 17544-17550 | If X is an instance of the hour Y, Z is an instance of the hour W, and equal the time X in zone mountain time zone and Z, then equal W and (Y and 7) |
| ! [V__UTC,V__H1,V__D,V__M,V__Y,V__CST,V__H2] : (((s__instance(V__UTC,s__TimePosition) & s__instance(V__H1,s__NonnegativeInteger) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__CST,s__TimePosition) & s__instance(V__H2,s__NonnegativeInteger)) => ((s__instance(V__UTC,s__HourFn(V__H1,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & s__instance(V__CST,s__HourFn(V__H2,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & (s__RelativeTimeFn(V__UTC,s__CentralTimeZone) = V__CST)) => (V__H2 = s__AdditionFn(V__H1,n__6)))) )
|
Merge.kif 17556-17562 | If X is an instance of the hour Y, Z is an instance of the hour W, and equal the time X in zone central time zone and Z, then equal W and (Y and 6) |
| ! [V__UTC,V__H1,V__D,V__M,V__Y,V__EST,V__H2] : (((s__instance(V__UTC,s__TimePosition) & s__instance(V__H1,s__NonnegativeInteger) & s__instance(V__D,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__EST,s__TimePosition) & s__instance(V__H2,s__NonnegativeInteger)) => ((s__instance(V__UTC,s__HourFn(V__H1,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & s__instance(V__EST,s__HourFn(V__H2,s__DayFn(V__D,s__MonthFn(V__M,s__YearFn(V__Y))))) & (s__RelativeTimeFn(V__UTC,s__EasternTimeZone) = V__EST)) => (V__H2 = s__AdditionFn(V__H1,n__5)))) )
|
Merge.kif 17568-17574 | If X is an instance of the hour Y, Z is an instance of the hour W, and equal the time X in zone eastern time zone and Z, then equal W and (Y and 5) |
| ! [V__D2,V__N2,V__M,V__Y,V__D1] : (((s__instance(V__D2,s__TimePosition) & s__instance(V__N2,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__D1,s__TimePosition)) => ((s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__temporalPart(V__D1,s__WeekBeforeFn(V__D2)) & s__temporalPart(V__D2,s__WeekAfterFn(V__D1))) => (? [V__N1] : ((s__instance(V__N1,s__PositiveInteger) & (s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))) & (V__N1 = s__SubtractionFn(V__N2,n__7)))))))) )
|
Mid-level-ontology.kif 16444-16453 | If X is an instance of the day Y of month the month Z, W is a part of week before fn X, and X is a part of week after fn W, then there exists V such that W is an instance of the day V of month the month Z and equal V and (Y and 7) |
| ! [V__A1 : $real,V__A2 : $real,V__B : $i,V__D : $int,V__F : $i,V__M : $i,V__START : $i,V__T : $i,V__Y : $int] : (((s__holdsDuring(V__T, s__attribute(V__F, s__Menopausal)) & s__birthdate(V__F, V__B) & s__instance(V__B, s__DayFn(V__D,s__MonthFn(V__M, s__YearFn(V__Y)))) & V__A1 = $sum(49 ,V__Y) & V__A2 = $sum(52 ,V__Y) & V__START = s__BeginFn(V__T)) => s__modalAttribute((($greater(V__START,V__A1)) & ($greater(V__A2,V__START))), s__Likely))) | Mid-level-ontology.kif 26201-26217 | If All of the following hold: (1) menopause is an attribute of X holds during Y (2) Z is a birthdate of X (3) Z is an instance of the day W of month the month V (4) equal U and (49 and T) (5) equal S and (52 and T) (6) equal R and the beginning of Y, then the statement R is greater than U and S is greater than R has the modal force of likely |
| ! [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 |
| ! [V__HOLIDAY,V__DAY,V__MONTH,V__YEAR,V__DATE,V__ANYO] : (((s__instance(V__HOLIDAY,s__Class) & s__subclass(V__HOLIDAY,s__Holiday) & s__instance(V__DAY,s__PositiveInteger) & s__subclass(V__MONTH,s__Month) & s__instance(V__YEAR,s__Integer) & s__instance(V__DATE,s__TimeInterval) & s__instance(V__ANYO,s__TimeInterval)) => ((s__commemoratesDate(V__HOLIDAY,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__YEAR)))) & s__instance(V__DATE,V__HOLIDAY) & s__instance(V__ANYO,s__YearFn(V__YEAR))) => ~(s__earlier(V__DATE,V__ANYO)))) )
|
Government.kif 576-581 | If the day X of month the month Y is a commemorates date of Z, W is an instance of Z, and V is an instance of the year U, then W doesn't happen earlier than V |
| ! [V__HOLIDAY,V__DAY,V__MONTH,V__YEAR,V__LATER_YEAR,V__DATE] : (((s__instance(V__HOLIDAY,s__Class) & s__subclass(V__HOLIDAY,s__Holiday) & s__instance(V__DAY,s__PositiveInteger) & s__subclass(V__MONTH,s__Month) & s__instance(V__YEAR,s__Integer) & s__instance(V__LATER_YEAR,s__Integer)) => ((s__commemoratesDate(V__HOLIDAY,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__YEAR)))) & s__instance(V__DATE,V__HOLIDAY) & s__subclass(V__HOLIDAY,s__FixedHoliday) & s__lessThanOrEqualTo(V__YEAR,V__LATER_YEAR)) => s__instance(V__DATE,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__LATER_YEAR)))))) )
|
Government.kif 583-589 | If the day X of month the month Y is a commemorates date of Z, W is an instance of Z, Z is a subclass of fixed holiday, and V is less than or equal to ?LATER_YEAR, then W is an instance of the day X of month the month Y |
| ! [V__DAY,V__Y1,V__Y2] : (((s__instance(V__DAY,s__Day) & s__instance(V__Y1,s__TimeInterval) & s__instance(V__Y2,s__TimeInterval)) => ((s__birthdate(s__JesusOfNazareth,V__DAY) & s__instance(V__Y1,s__YearFn(n___6)) & s__instance(V__Y2,s__YearFn(n__4))) => s__temporalPart(V__DAY,s__TimeIntervalFn(s__BeginFn(V__Y1) ,s__EndFn(V__Y2))))) )
|
Media.kif 1883-1888 | If X is a birthdate of Jesus of Nazareth, Y is an instance of the year -6, and Z is an instance of the year 4, then X is a part of interval between the beginning of Y and the end of Z |
| ! [V__DAY,V__Y1,V__Y2] : (((s__instance(V__DAY,s__Day) & s__instance(V__Y1,s__TimeInterval) & s__instance(V__Y2,s__TimeInterval)) => ((s__deathdate(s__JesusOfNazareth,V__DAY) & s__instance(V__Y1,s__YearFn(n__29)) & s__instance(V__Y2,s__YearFn(n__36))) => s__temporalPart(V__DAY,s__TimeIntervalFn(s__BeginFn(V__Y1) ,s__EndFn(V__Y2))))) )
|
Media.kif 1890-1895 | If X is a deathdate of Jesus of Nazareth, Y is an instance of the year 29, and Z is an instance of the year 36, then X is a part of interval between the beginning of Y and the end of Z |
| ! [V__T1,V__T2] : (((s__instance(V__T1,s__TimeInterval) & s__instance(V__T2,s__TimeInterval)) => ((s__instance(V__T1,s__YearFn(n__26)) & s__instance(V__T2,s__YearFn(n__100))) => s__temporalPart(s__WhenFn(s__TwelveApostles),s__TimeIntervalFn(s__BeginFn(V__T1) ,s__EndFn(V__T2))))) )
|
Media.kif 1906-1910 | If X is an instance of the year 26 and Y is an instance of the year 100, then the time of existence of Twelve apostles is a part of interval between the beginning of X and the end of Y |
| ! [V__ADJUSTEDPERCENT : $real,V__AREA : $i,V__PERCENT : $int,V__POPULATION : $int,V__PREVIOUSPOPULATION : $int,V__PREVIOUSYEAR : $i,V__Y : $int,V__YEAR : $i,V__YP : $int] : ((((s__instance(V__YEAR, s__YearFn(V__Y)) & s__PopulationGrowthFn(V__AREA, V__YEAR) = V__ADJUSTEDPERCENT) => ($difference(V__Y ,V__YP) = 1 & s__instance(V__PREVIOUSYEAR, s__YearFn(V__YP)) & s__holdsDuring(V__YEAR, s__PopulationFn(V__AREA) = V__POPULATION) & s__holdsDuring(V__PREVIOUSYEAR, s__PopulationFn(V__AREA) = V__PREVIOUSPOPULATION) & s__DivisionFn(V__POPULATION, V__PREVIOUSPOPULATION) = V__PERCENT & $difference(V__PERCENT ,1) = V__ADJUSTEDPERCENT)) & (($difference(V__Y ,V__YP) = 1 & s__instance(V__PREVIOUSYEAR, s__YearFn(V__YP)) & s__holdsDuring(V__YEAR, s__PopulationFn(V__AREA) = V__POPULATION) & s__holdsDuring(V__PREVIOUSYEAR, s__PopulationFn(V__AREA) = V__PREVIOUSPOPULATION) & s__DivisionFn(V__POPULATION, V__PREVIOUSPOPULATION) = V__PERCENT & $difference(V__PERCENT ,1) = V__ADJUSTEDPERCENT) => (s__instance(V__YEAR, s__YearFn(V__Y)) & s__PopulationGrowthFn(V__AREA, V__YEAR) = V__ADJUSTEDPERCENT)))) | People.kif 52-64 | X is an instance of the year Y and equal the population growth of Z and X and W if and only if equal (Y and V) and 1 and U is an instance of the year V and equal the population of Z and T holds during X and equal the population of Z and S holds during U and equal T and S and R and equal (R and 1) and W |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__O,V__Y] : (((s__instance(V__O,s__Organization) & s__instance(V__Y,s__Integer)) => (s__yearOfFounding(V__O,V__Y) => s__dateEstablished(V__O,s__YearFn(V__Y)))) )
|
Mid-level-ontology.kif 950-953 | If X is a year of founding of Y, then the year X is a date established of Y |
| ! [V__O,V__Y] : (((s__instance(V__O,s__Organization) & s__instance(V__Y,s__Integer)) => ((s__yearOfFounding(V__O,V__Y) => (? [V__F,V__YEAR] : ((s__instance(V__YEAR,s__TimeInterval) & (s__overlapsTemporally(s__WhenFn(V__F) ,V__YEAR) & s__instance(V__YEAR,s__YearFn(V__Y)) & s__instance(V__F,s__Founding) & s__result(V__F,V__O)))))) & ((? [V__F,V__YEAR] : ((s__instance(V__YEAR,s__TimeInterval) & (s__overlapsTemporally(s__WhenFn(V__F) ,V__YEAR) & s__instance(V__YEAR,s__YearFn(V__Y)) & s__instance(V__F,s__Founding) & s__result(V__F,V__O))))) => s__yearOfFounding(V__O,V__Y)))) )
|
Mid-level-ontology.kif 958-965 | X is a year of founding of Y if, only if there exist Z, W such that W overlaps the time of existence of Z, W is an instance of the year X, Z is an instance of founding, and Y is a result of Z |
| ! [V__D2,V__N2,V__M,V__Y,V__D1] : (((s__instance(V__D2,s__TimePosition) & s__instance(V__N2,s__PositiveInteger) & s__subclass(V__M,s__Month) & s__instance(V__Y,s__Integer) & s__instance(V__D1,s__TimePosition)) => ((s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y)))) & s__temporalPart(V__D1,s__WeekBeforeFn(V__D2)) & s__temporalPart(V__D2,s__WeekAfterFn(V__D1))) => (? [V__N1] : ((s__instance(V__N1,s__PositiveInteger) & (s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y)))) & (V__N1 = s__SubtractionFn(V__N2,n__7)))))))) )
|
Mid-level-ontology.kif 16444-16453 | If X is an instance of the day Y of month the month Z, W is a part of week before fn X, and X is a part of week after fn W, then there exists V such that W is an instance of the day V of month the month Z and equal V and (Y and 7) |
| ! [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 |
| ! [V__HOLIDAY,V__DAY,V__MONTH,V__YEAR,V__LATER_YEAR,V__DATE] : (((s__instance(V__HOLIDAY,s__Class) & s__subclass(V__HOLIDAY,s__Holiday) & s__instance(V__DAY,s__PositiveInteger) & s__subclass(V__MONTH,s__Month) & s__instance(V__YEAR,s__Integer) & s__instance(V__LATER_YEAR,s__Integer)) => ((s__commemoratesDate(V__HOLIDAY,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__YEAR)))) & s__instance(V__DATE,V__HOLIDAY) & s__subclass(V__HOLIDAY,s__FixedHoliday) & s__lessThanOrEqualTo(V__YEAR,V__LATER_YEAR)) => s__instance(V__DATE,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__LATER_YEAR)))))) )
|
Government.kif 583-589 | If the day X of month the month Y is a commemorates date of Z, W is an instance of Z, Z is a subclass of fixed holiday, and V is less than or equal to ?LATER_YEAR, then W is an instance of the day X of month the month Y |
| ! [V__D : $i,V__H : $i,V__T : $i] : ((s__holdsDuring(V__T, (s__instance(V__D, s__DeltaCovidVariant) & s__part(V__D, V__H) & s__attribute(V__H, s__Covid19))) => ($greater(V__T,s__MonthFn(s__December, s__YearFn(2020)))))) | Medicine.kif 3009-3017 | If X is an instance of delta, X is a part of Y, and Covid is an attribute of Y holds during Z, then Z is greater than the month December |
| ! [V__ADJUSTEDPERCENT : $real,V__AREA : $i,V__PERCENT : $int,V__POPULATION : $int,V__PREVIOUSPOPULATION : $int,V__PREVIOUSYEAR : $i,V__Y : $int,V__YEAR : $i,V__YP : $int] : ((((s__instance(V__YEAR, s__YearFn(V__Y)) & s__PopulationGrowthFn(V__AREA, V__YEAR) = V__ADJUSTEDPERCENT) => ($difference(V__Y ,V__YP) = 1 & s__instance(V__PREVIOUSYEAR, s__YearFn(V__YP)) & s__holdsDuring(V__YEAR, s__PopulationFn(V__AREA) = V__POPULATION) & s__holdsDuring(V__PREVIOUSYEAR, s__PopulationFn(V__AREA) = V__PREVIOUSPOPULATION) & s__DivisionFn(V__POPULATION, V__PREVIOUSPOPULATION) = V__PERCENT & $difference(V__PERCENT ,1) = V__ADJUSTEDPERCENT)) & (($difference(V__Y ,V__YP) = 1 & s__instance(V__PREVIOUSYEAR, s__YearFn(V__YP)) & s__holdsDuring(V__YEAR, s__PopulationFn(V__AREA) = V__POPULATION) & s__holdsDuring(V__PREVIOUSYEAR, s__PopulationFn(V__AREA) = V__PREVIOUSPOPULATION) & s__DivisionFn(V__POPULATION, V__PREVIOUSPOPULATION) = V__PERCENT & $difference(V__PERCENT ,1) = V__ADJUSTEDPERCENT) => (s__instance(V__YEAR, s__YearFn(V__Y)) & s__PopulationGrowthFn(V__AREA, V__YEAR) = V__ADJUSTEDPERCENT)))) | People.kif 52-64 | X is an instance of the year Y and equal the population growth of Z and X and W if and only if equal (Y and V) and 1 and U is an instance of the year V and equal the population of Z and T holds during X and equal the population of Z and S holds during U and equal T and S and R and equal (R and 1) and W |
| ! [V__AREA : $i,V__BIRTH : $i,V__BIRTHCOUNT : $int,V__INFANT : $i,V__REALNUMBER : $real,V__THOUSANDS : $real,V__Y : $int,V__YEAR : $i] : (((s__DivisionFn(s__PopulationFn(V__AREA), 1000) = V__THOUSANDS & V__BIRTHCOUNT = s__CardinalityFn(s__KappaFn(V__BIRTH, (s__instance(V__BIRTH, s__Birth) & s__experiencer(V__BIRTH, V__INFANT) & s__instance(V__INFANT, s__Human) & s__during(s__WhenFn(V__BIRTH), V__YEAR) & s__WhereFn(V__BIRTH, s__WhenFn(V__BIRTH)) = V__AREA))) & s__DivisionFn(V__BIRTHCOUNT, V__THOUSANDS) = V__REALNUMBER) => (s__instance(V__YEAR, s__YearFn(V__Y)) & s__BirthsPerThousandFn(V__AREA, V__YEAR) = V__REALNUMBER))) | People.kif 99-114 | If equal the population of X, 1000, and Y, equal Z and the number of instances in the class described by W, and equal Z, Y, and V, then U is an instance of the year T and equal the births per thousand of X, U, and V |
| ! [V__AREA : $i,V__DEATH : $i,V__DEATHCOUNT : $int,V__PERSON : $i,V__REALNUMBER : $real,V__THOUSANDS : $real,V__Y : $int,V__YEAR : $i] : (((s__DivisionFn(s__PopulationFn(V__AREA), 1000) = V__THOUSANDS & V__DEATHCOUNT = s__CardinalityFn(s__KappaFn(V__DEATH, (s__instance(V__DEATH, s__Death) & s__experiencer(V__DEATH, V__PERSON) & s__instance(V__PERSON, s__Human) & s__during(s__WhenFn(V__DEATH), V__YEAR) & s__WhereFn(V__DEATH, s__WhenFn(V__DEATH)) = V__AREA))) & s__DivisionFn(V__DEATHCOUNT, V__THOUSANDS) = V__REALNUMBER) => (s__instance(V__YEAR, s__YearFn(V__Y)) & s__DeathsPerThousandFn(V__AREA, V__YEAR) = V__REALNUMBER))) | People.kif 152-167 | If equal the population of X, 1000, and Y, equal Z and the number of instances in the class described by W, and equal Z, Y, and V, then U is an instance of the year T and equal the deaths per thousand of X, U, and V |
| ! [V__AREA : $i,V__EMMIGRATION : $int,V__IMMIGRATION : $int,V__MIGRATIONCOUNT : $real,V__PERSON : $i,V__POPULATION : $int,V__PREVIOUSYEAR : $i,V__PY : $int,V__REALNUMBER : $real,V__THOUSANDS : $real,V__Y : $int,V__YEAR : $i] : (((s__instance(V__YEAR, s__YearFn(V__Y)) & s__MigrantsPerThousandFn(V__AREA, V__YEAR) = V__REALNUMBER) => ($difference(V__Y ,V__PY) = 1 & s__instance(V__PREVIOUSYEAR, s__YearFn(V__PY)) & s__holdsDuring(V__YEAR, s__PopulationFn(V__AREA) = V__POPULATION) & s__DivisionFn(V__POPULATION, 1000) = V__THOUSANDS & V__IMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__holdsDuring(V__PREVIOUSYEAR, ~(s__inhabits(V__PERSON, V__AREA))) & s__holdsDuring(V__YEAR, s__inhabits(V__PERSON, V__AREA))))) & V__EMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__holdsDuring(V__PREVIOUSYEAR, s__inhabits(V__PERSON, V__AREA)) & s__holdsDuring(V__YEAR, ~(s__inhabits(V__PERSON, V__AREA)))))) & $difference(V__IMMIGRATION ,V__EMMIGRATION) = V__MIGRATIONCOUNT & s__DivisionFn(V__MIGRATIONCOUNT, V__THOUSANDS) = V__REALNUMBER))) | People.kif 190-221 | If X is an instance of the year Y and equal the migrants per thousand of Z, X, and W, then All of the following hold: (1) equal (Y and V) and 1 (2) U is an instance of the year V (3) equal the population of Z and T holds during X (4) equal T, 1000, and S (5) equal R and the number of instances in the class described by Q (6) equal P and the number of instances in the class described by Q (7) equal (R and P) and O (8) equal O, S, and W |
| ! [V__M1,V__Y1,V__M2,V__Y2,V__I] : (((s__subclass(V__M1,s__Month) & s__instance(V__Y1,s__Year) & s__subclass(V__M2,s__Month) & s__instance(V__Y2,s__Year) & s__instance(V__I,s__Integer)) => ((s__previousMonthYear(V__M1,V__Y1,V__M2,V__Y2) & s__instance(V__Y2,s__YearFn(V__I)) & (V__M2 = s__MonthFn(s__January,s__YearFn(V__I)))) => ((V__M1 = s__December) & s__instance(V__Y1,s__YearFn(s__SubtractionFn(V__I,n__1)))))) )
|
Weather.kif 762-773 | If the previous month of X in year Y is Z W, Y is an instance of the year V, and equal X and the month January, then equal Z and December and W is an instance of the year (V and 1) |
| ! [V__HS,V__HE,V__H] : (((s__instance(V__HS,s__TimeInterval) & s__instance(V__HE,s__TimeInterval)) => (s__instance(V__H,s__HarmattanSeason) => (? [V__Y] : ((s__instance(V__Y,s__Integer) & (s__instance(V__HS,s__MonthFn(s__November,s__YearFn(V__Y))) & s__instance(V__HE,s__MonthFn(s__March,s__YearFn(s__AdditionFn(V__Y,n__1)))) & s__during(V__H,s__IntervalFn(s__EndFn(V__HS) ,s__BeginFn(V__HE))))))))) )
|
Weather.kif 2037-2050 | If X is an instance of Harmattan season, then there exists Y such that Z is an instance of the month November, W is an instance of the month March, and X takes place during the interval from the end of Z to the beginning of W |
| ! [V__TIMEINTERVAL1,V__YEAR,V__STUDENT,V__SCHOOL,V__GRADUATE] : (((s__instance(V__TIMEINTERVAL1,s__Physical) & s__instance(V__TIMEINTERVAL1,s__TimeInterval) & s__instance(V__YEAR,s__Integer)) => ((s__instance(V__STUDENT,s__Student) & s__instance(V__SCHOOL,s__School) & s__attends(V__STUDENT,V__SCHOOL) & s__instance(V__GRADUATE,s__Graduation) & s__time(V__TIMEINTERVAL1,V__GRADUATE) & s__agent(V__GRADUATE,V__SCHOOL) & s__patient(V__GRADUATE,V__STUDENT) & s__during(V__TIMEINTERVAL1,s__YearFn(V__YEAR))) => s__expectedYearOfGraduation(V__STUDENT,s__YearFn(V__YEAR)))) )
|
LinkedInDegrees.kif 450-461 | If All of the following hold: (1) X is an instance of student (2) Y is an instance of school (3) Y attends X (4) Z is an instance of graduation (5) W exists during Z (6) Y is an agent of Z (7) X is a patient of Z (8) W takes place during the year V, then expectedYearOfGraduation X and the year V |
| statement |
|
|
|