NightTime | ![]() |
appearance as argument number 1 |
![]() |
(documentation NightTime EnglishLanguage "The class of TimeIntervals that begin at Sunset and end at Sunrise.") | Merge.kif 9002-9003 | |
(subclass NightTime TimeInterval) | Merge.kif 9001-9001 |
appearance as argument number 2 |
![]() |
(disjoint DayTime NightTime) | Merge.kif 8973-8973 | |
(subclass Evening NightTime) | Merge.kif 9023-9023 | |
(termFormat ChineseLanguage NightTime "晚上的时间") | domainEnglishFormat.kif 40564-40564 | |
(termFormat ChineseTraditionalLanguage NightTime "晚上的時間") | domainEnglishFormat.kif 40563-40563 | |
(termFormat EnglishLanguage NightTime "night time") | domainEnglishFormat.kif 40562-40562 |
antecedent |
![]() |
(=> (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 3579-3600 | |
(=> (instance ?NIGHT NightTime) (exists (?DAY1 ?DAY2) (and (instance ?DAY1 DayTime) (instance ?DAY2 DayTime) (meetsTemporally ?NIGHT ?DAY1) (meetsTemporally ?DAY2 ?NIGHT)))) |
Merge.kif 9005-9012 | |
(=> (instance ?NIGHT NightTime) (exists (?RISE ?SET) (and (instance ?RISE Sunrise) (instance ?SET Sunset) (starts ?SET ?NIGHT) (finishes ?RISE ?NIGHT)))) |
Merge.kif 9014-9021 |
consequent |
![]() |
(=> (and (instance ?X NightClub) (standardRetailHours ?TIME ?X)) (exists (?T) (and (instance ?T ?TIME) (during ?T NightTime)))) |
Dining.kif 419-426 | |
(=> (instance ?DAY DayTime) (exists (?NIGHT1 ?NIGHT2) (and (instance ?NIGHT1 NightTime) (instance ?NIGHT2 NightTime) (meetsTemporally ?DAY ?NIGHT1) (meetsTemporally ?NIGHT2 ?DAY)))) |
Merge.kif 8983-8990 | |
(=> (instance ?TIME DinnerTime) (exists (?NIGHT) (and (instance ?NIGHT NightTime) (during ?TIME ?NIGHT)))) |
Food.kif 1890-1895 |
![]() |
![]() |