Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| NightTime(night time) |  | Bonfire_Night, Guy_Fawkes_Night, dark, night, nighttime, small_hours, this_evening, this_night, tonight |
| appearance as argument number 1 |
|
|
| (subclass NightTime TimeInterval) | Merge.kif 9090-9090 | Night time is a subclass of timeframe |
| (documentation NightTime EnglishLanguage "The class of TimeIntervals that begin at Sunset and end at Sunrise.") | Merge.kif 9091-9092 | Night time is a subclass of timeframe |
| appearance as argument number 2 |
|
|
| (disjoint DayTime NightTime) | Merge.kif 9062-9062 | Day time is disjoint from night time |
| (subclass Evening NightTime) | Merge.kif 9112-9112 | Evening is a subclass of night time |
| (termFormat EnglishLanguage NightTime "night time") | domainEnglishFormat.kif 40555-40555 | Evening is a subclass of night time |
| (termFormat ChineseTraditionalLanguage NightTime "晚上的時間") | domainEnglishFormat.kif 40556-40556 | Evening is a subclass of night time |
| (termFormat ChineseLanguage NightTime "晚上的时间") | domainEnglishFormat.kif 40557-40557 | Evening is a subclass of night time |
| antecedent |
|
|
| (=> (instance ?NIGHT NightTime) (exists (?DAY1 ?DAY2) (and (instance ?DAY1 DayTime) (instance ?DAY2 DayTime) (meetsTemporally ?NIGHT ?DAY1) (meetsTemporally ?DAY2 ?NIGHT)))) |
Merge.kif 9094-9101 | If X is an instance of night time, then there exist Y, Z such that Y is an instance of day time, Z is an instance of day time, X meets Y, and Z meets X |
| (=> (instance ?NIGHT NightTime) (exists (?RISE ?SET) (and (instance ?RISE Sunrise) (instance ?SET Sunset) (starts ?SET ?NIGHT) (finishes ?RISE ?NIGHT)))) |
Merge.kif 9103-9110 | If X is an instance of night time, then there exist Y, Z such that Y is an instance of sunrise, Z is an instance of sunset, Z starts X, and Y finishes X |
| (=> (and (visibilityInMeteorology ?Area ?Time (MeasureFn ?Distance ?U)) (instance ?U UnitOfMeasure) (instance ?Time NightTime) (instance ?Observe Looking) (instance ?B Region) (attribute ?B Illuminated) (measure ?B (MeasureFn 1000.0 Candela)) (agent ?Observe ?A) (patient ?Observe ?B) (orientation ?A ?B Horizontal) (eventLocated ?Observe ?Area) (during (WhenFn ?Observe) ?Time) (instance ?B Object)) (exists (?D2) (and (distance ?A ?B (MeasureFn ?D2 ?U)) (greaterThan ?Distance ?D2)))) |
Weather.kif 4017-4038 | If All of the following hold: (1) the visibility at X during Y is Z W(s) (2) W is an instance of unit of measure (3) Y is an instance of night time (4) V is an instance of looking (5) U is an instance of region (6) illuminated is an attribute of U (7) the measure of U is 1000.0 candela(s) (8) T is an agent of V (9) U is a patient of V (10) T is horizontal to to U (11) V is located at X (12) the time of existence of V takes place during Y (13) U is an instance of object, then there exists S such that the distance between T and U is S W(s) and Z is greater than S |
| consequent |
|
|
| (=> (instance ?DAY DayTime) (exists (?NIGHT1 ?NIGHT2) (and (instance ?NIGHT1 NightTime) (instance ?NIGHT2 NightTime) (meetsTemporally ?DAY ?NIGHT1) (meetsTemporally ?NIGHT2 ?DAY)))) |
Merge.kif 9072-9079 | If X is an instance of day time, then there exist Y, Z such that Y is an instance of night time, Z is an instance of night time, X meets Y, and Z meets X |
| (=> (and (instance ?X NightClub) (standardRetailHours ?TIME ?X)) (exists (?T) (and (instance ?T ?TIME) (during ?T NightTime)))) |
Dining.kif 419-426 | If X is an instance of night club and the standard retail hours for X are Y, then there exists Z such that Z is an instance of Y and Z takes place during night time |
| (=> (instance ?TIME DinnerTime) (exists (?NIGHT) (and (instance ?NIGHT NightTime) (during ?TIME ?NIGHT)))) |
Food.kif 1897-1902 | If X is an instance of dinner time, then there exists Y such that Y is an instance of night time and X takes place during Y |
|