Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| TimePosition(time position) |  | 4-dimensional, TRM, actual, actually, arrival_time, back, bedtime, beginning, change_of_life, checkout, checkout_time, climacteric, clock_time, commencement, curfew, current, date, dawn, day, deadline, deep, departure_time, equinoctial, evening, first, four-dimensional, full_term, get-go, immediate, in_reality, just_then, kickoff, latter-day, lights-out, limitation, meal, menopause, meridian, middle, midweek, nonce, noncurrent, occasion, offset, on-going, ongoing, outset, particular_date, pinpoint, showtime... |
| appearance as argument number 1 |
|
|
| s__subclass(s__TimePosition,s__TimeMeasure)
|
Merge.kif 2188-2188 | Time position is a subclass of time measure |
| s__partition(s__TimePosition,s__TimeInterval,s__TimePoint)
|
Merge.kif 2189-2189 | Time position is exhaustively partitioned into timeframe and time point |
| s__documentation(s__TimePosition, s__EnglishLanguage, "Any TimePoint or TimeInterval along the universal timeline from NegativeInfinity to PositiveInfinity_") | Merge.kif 2191-2192 | Time position is exhaustively partitioned into timeframe and time point |
| appearance as argument number 2 |
|
|
| s__subclass(s__TimeInterval,s__TimePosition)
|
Merge.kif 2194-2194 | Timeframe is a subclass of time position |
| s__subclass(s__TimePoint,s__TimePosition)
|
Merge.kif 2201-2201 | Time point is a subclass of time position |
| s__range(s__RelativeTimeFn,s__TimePosition)
|
Merge.kif 17581-17581 | The range of relative time is an instance of time position |
| s__termFormat(s__EnglishLanguage, s__TimePosition, "time position") | english_format.kif 964-964 | The range of relative time is an instance of time position |
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| ! [V__AGENT1 : $i,V__AGENT2 : $i,V__OBJ : $i,V__TIME : $i] : (((s__instance(V__TIME, s__TimePosition) & s__holdsDuring(V__TIME, s__possesses(V__AGENT1, V__OBJ)) & s__holdsDuring(V__TIME, s__possesses(V__AGENT2, V__OBJ))) => V__AGENT1 = V__AGENT2)) | Merge.kif 4379-4384 | If X is an instance of time position, Y possesses Z holds during X, and W possesses Z holds during X, then equal Y and W |
| ! [V__INTERVAL1,V__INTERVAL2,V__INTERVAL3] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => ((s__instance(V__INTERVAL3,s__TimePosition) & s__temporalPart(V__INTERVAL3,V__INTERVAL1) & s__temporalPart(V__INTERVAL3,V__INTERVAL2)) => s__overlapsTemporally(V__INTERVAL1,V__INTERVAL2))) )
|
Merge.kif 8500-8505 | If X is an instance of time position, X is a part of Y, and X is a part of Z, then Z overlaps Y |
| ! [V__AREA : $i,V__TEMP : $real,V__TIME : $i] : (((s__climateTypeInArea(V__AREA, s__PolarTypeFClimateZone) & s__instance(V__TIME, s__TimePosition) & s__holdsDuring(V__TIME, s__airTemperature(V__AREA, s__MeasureFn(V__TEMP, s__CelsiusDegree)))) => s__holdsDuring(V__TIME, ($greater(10.0,V__TEMP))))) | Geography.kif 3054-3060 | If polar typeF climate zone is a climate type in area of X, Y is an instance of time position, and Z celsius degree(s) is an air temperature of X holds during Y, then 10.0 is greater than Z holds during Y |
| consequent |
|
|
| ! [V__INTERVAL1,V__INTERVAL2] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval)) => (s__overlapsTemporally(V__INTERVAL1,V__INTERVAL2) => (? [V__INTERVAL3] : ((s__instance(V__INTERVAL3,s__TimePosition) & s__temporalPart(V__INTERVAL3,V__INTERVAL1) & s__temporalPart(V__INTERVAL3,V__INTERVAL2)))))) )
|
Merge.kif 8492-8498 | If X overlaps Y, then there exists Z such that Z is an instance of time position, Z is a part of Y, and Z is a part of X |
|