Afternoon - Sigma Knowledge base Browser

antecedent

(=> (instance ?AFTERNOON Afternoon) (exists (?HOUR ?DAY) (and (instance ?HOUR (HourFn 12 ?DAY)) (starts ?HOUR ?AFTERNOON))))	Merge.kif 8997-9003	If X is an instance of afternoon, then there exist Y, Z such that Y is an instance of the hour 12, and Y starts X
(=> (and (instance ?E Afternoon) (instance ?D Day) (equal ?E (AfternoonFn ?D))) (during ?E ?D))	Merge.kif 9042-9047	If X is an instance of afternoon, Y is an instance of day, and equal X and the afternoon of Y, then X takes place during Y
(=> (instance ?A Afternoon) (exists (?N) (and (instance ?N Noon) (equal (BeginFn ?A) ?N))))	Merge.kif 9049-9054	If X is an instance of afternoon, then there exists Y such that Y is an instance of noon, equal the beginning of X, and Y
(=> (and (instance ?EVE Evening) (instance ?AFT Afternoon) (instance ?D Day) (during ?EVE ?D) (during ?AFT ?D)) (meetsTemporally ?AFT ?EVE))	Merge.kif 9124-9131	If X is an instance of evening, Y is an instance of afternoon, Z is an instance of day, X takes place during Z, and Y takes place during Z, then Y meets X

(subclass Afternoon DayTime)	Merge.kif 8990-8990	Afternoon is a subclass of day time
(documentation Afternoon EnglishLanguage "The class of TimeIntervals that begin at noon and end at Sunset.")	Merge.kif 8991-8992	Afternoon is a subclass of day time
(disjoint Afternoon Evening)	Merge.kif 8994-8994	Afternoon is disjoint from evening

(disjoint Morning Afternoon)	Merge.kif 8993-8993	Morning is disjoint from afternoon
(range AfternoonFn Afternoon)	Merge.kif 9037-9037	The range of afternoon of is an instance of afternoon
(termFormat EnglishLanguage Afternoon "afternoon")	domainEnglishFormat.kif 5773-5773	The range of afternoon of is an instance of afternoon
(termFormat ChineseTraditionalLanguage Afternoon "下午")	domainEnglishFormat.kif 5774-5774	The range of afternoon of is an instance of afternoon
(termFormat ChineseLanguage Afternoon "下午")	domainEnglishFormat.kif 5775-5775	The range of afternoon of is an instance of afternoon