more pictures...
| appearance as argument number 1 |
|
|
| appearance as argument number 2 |
|
|
| (subclass ChristmasDay Day) | Media.kif 335-335 | Christmas day is a subclass of day |
| (rangeSubclass DayFn Day) | Merge.kif 8723-8723 | The values returned by day are subclasses of day |
| (subclass Monday Day) | Merge.kif 9373-9373 | Monday is a subclass of day |
| (subclass Tuesday Day) | Merge.kif 9385-9385 | Tuesday is a subclass of day |
| (subclass Wednesday Day) | Merge.kif 9398-9398 | Wednesday is a subclass of day |
| (subclass Thursday Day) | Merge.kif 9411-9411 | Thursday is a subclass of day |
| (subclass Friday Day) | Merge.kif 9424-9424 | Friday is a subclass of day |
| (subclass Saturday Day) | Merge.kif 9437-9437 | Saturday is a subclass of day |
| (subclass Sunday Day) | Merge.kif 9450-9450 | Sunday is a subclass of day |
| (termFormat EnglishLanguage Day "day") | english_format.kif 1795-1795 | Sunday is a subclass of day |
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| (=> (and (instance ?H Man) (attribute ?H Mausaharati) (instance ?D Drumming) (agent ?D ?H) (instance ?DAY Day) (instance ?S Sunrise) (during ?S ?DAY) (earlier (WhenFn ?D) ?S)) (hasPurpose ?D (exists (?P ?SUHUR ?WU) (and (instance ?WU WakingUp) (experiencer ?WU ?P) (instance ?SUHUR Suhur) (agent ?SUHUR ?P) (earlier (WhenFn ?WU) (WhenFn ?SUHUR)) (during (WhenFn ?WU) ?DAY) (during (WhenFn ?SUHUR) ?DAY))))) |
ArabicCulture.kif 65-84 | If All of the following hold: (1) X is an instance of man (2) mausaharati is an attribute of X (3) Y is an instance of drumming (4) X is an agent of Y (5) Z is an instance of day (6) W is an instance of sunrise (7) W takes place during Z (8) the time of existence of Y happens earlier than W, then All of the following hold: (1) Y has the purpose there exist V, U (2) T such that T is an instance of waking up (3) V experiences T (4) U is an instance of suhur (5) V is an agent of U (6) the time of existence of T happens earlier than the time of existence of U (7) the time of existence of T takes place during Z (8) the time of existence of U takes place during Z |
| (=> (and (instance ?LOW LowTide) (instance ?HIGH HighTide) (eventLocated ?LOW ?PLACE) (eventLocated ?HIGH ?PLACE) (instance ?DAY Day) (overlapsTemporally ?LOW ?DAY) (overlapsTemporally ?HIGH ?DAY)) (exists (?AMOUNT1 ?AMOUNT2 ?U) (and (instance ?U UnitOfLength) (holdsDuring ?LOW (waterDepth ?PLACE (MeasureFn ?AMOUNT1 ?U))) (holdsDuring ?HIGH (waterDepth ?PLACE (MeasureFn ?AMOUNT2 ?U))) (greaterThan ?AMOUNT2 ?AMOUNT1)))) |
Geography.kif 6530-6548 | If All of the following hold: (1) X is an instance of low tide (2) Y is an instance of high tide (3) X is located at Z (4) Y is located at Z (5) W is an instance of day (6) W overlaps X (7) W overlaps Y, then there exist V, U and T such that T is an instance of unit of length and V T(s) is a water depth of Z holds during X and U T(s) is a water depth of Z holds during Y and U is greater than V |
| (=> (and (lowTide ?PLACE ?TIME1 (MeasureFn ?AMOUNT1 ?U)) (highTide ?PLACE ?TIME2 (MeasureFn ?AMOUNT2 ?U)) (instance ?U UnitOfLength) (instance ?DAY Day) (overlapsTemporally ?TIME1 ?DAY) (overlapsTemporally ?TIME2 ?DAY)) (greaterThan ?AMOUNT1 ?AMOUNT2)) |
Geography.kif 6599-6609 | If All of the following hold: (1) X low tide Y for Z W(s) (2) X is high tide V for U W(s) (3) W is an instance of unit of length (4) T is an instance of day (5) T overlaps Y (6) T overlaps V, then Z is greater than U |
| (=> (and (instance ?E Morning) (instance ?D Day) (equal ?E (MorningFn ?D))) (during ?E ?D)) |
Merge.kif 8957-8962 | If X is an instance of morning, Y is an instance of day, and equal X and the morning of Y, then X takes place during Y |
| (=> (and (instance ?E Afternoon) (instance ?D Day) (equal ?E (AfternoonFn ?D))) (during ?E ?D)) |
Merge.kif 8973-8978 | 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 |
| (=> (and (instance ?EVE Evening) (instance ?AFT Afternoon) (instance ?D Day) (during ?EVE ?D) (during ?AFT ?D)) (meetsTemporally ?AFT ?EVE)) |
Merge.kif 9055-9062 | 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 |
| (=> (and (instance ?E Evening) (instance ?D Day) (equal ?E (EveningFn ?D))) (during ?E ?D)) |
Merge.kif 9073-9078 | If X is an instance of evening, Y is an instance of day, and equal X and the evening of Y, then X takes place during Y |
| (=> (instance ?DAY Day) (duration ?DAY (MeasureFn 1 DayDuration))) |
Merge.kif 9369-9371 | If X is an instance of day, then duration of X is 1 day duration(s) |
| (=> (instance ?DAY Day) (equal (CardinalityFn (TemporalCompositionFn ?DAY Hour)) 24)) |
Merge.kif 9629-9631 | If X is an instance of day, then equal the number of instances in decomposition of X into hours and 24 |
| consequent |
|
|
| (=> (instance ?X Suhur) (exists (?R ?S ?D) (and (instance ?S Sunrise) (instance ?R Ramadan) (instance ?D Day) (during ?D ?R) (during (WhenFn ?X) ?D) (during ?S ?D) (before (WhenFn ?X) ?S)))) |
ArabicCulture.kif 36-46 | If X is an instance of suhur, then All of the following hold: (1) there exist Y, Z (2) W such that Z is an instance of sunrise (3) Y is an instance of ramadan (4) W is an instance of day (5) W takes place during Y (6) the time of existence of X takes place during W (7) Z takes place during W (8) the time of existence of X happens before Z |
| (=> (instance ?X Iftar) (exists (?R ?S ?D) (and (instance ?S Sunset) (instance ?R Ramadan) (instance ?D Day) (during ?D ?R) (during (WhenFn ?X) ?D) (during ?S ?D) (before ?S (WhenFn ?X))))) |
ArabicCulture.kif 91-101 | If X is an instance of iftar, then All of the following hold: (1) there exist Y, Z (2) W such that Z is an instance of sunset (3) Y is an instance of ramadan (4) W is an instance of day (5) W takes place during Y (6) the time of existence of X takes place during W (7) Z takes place during W (8) Z happens before the time of existence of X |
| (=> (and (instance ?TEXT BirthCertificate) (instance ?B Birth) (instance ?A Human) (experiencer ?B ?A)) (containsFormula ?TEXT (exists (?DAY ?P ?N) (and (birthdate ?A ?DAY) (instance ?DAY Day) (birthplace ?A ?P) (instance ?P GeographicArea) (represents ?N ?A) (instance ?N Name))))) |
Biography.kif 256-270 | If X is an instance of birth certificate, Y is an instance of birth, Z is an instance of human, and Z experiences Y, then All of the following hold: (1) X contains the formula there exist W, V (2) U such that W is a birthdate of Z (3) W is an instance of day (4) V is a birthplace of Z (5) V is an instance of geographic area (6) U expresses Z (7) U is an instance of name |
| (=> (and (instance ?TEXT DeathCertificate) (instance ?D Death) (instance ?A Human) (experiencer ?D ?A)) (containsFormula ?TEXT (exists (?DAY ?P ?N ?PROC) (and (deathdate ?A ?DAY) (instance ?DAY Day) (deathplace ?A ?P) (instance ?P GeographicArea) (represents ?N ?A) (instance ?N Name) (causes ?PROC ?D) (instance ?PROC Process))))) |
Biography.kif 287-303 | If X is an instance of death certificate, Y is an instance of death, Z is an instance of human, and Z experiences Y, then All of the following hold: (1) X contains the formula there exist W, V,, , U (2) T such that W is a deathdate of Z (3) W is an instance of day (4) V is a deathplace of Z (5) V is an instance of geographic area (6) U expresses Z (7) U is an instance of name (8) T causes Y (9) T is an instance of process |
| (=> (and (instance ?TEXT MarriageCertificate) (instance ?A Human) (instance ?B Human) (spouse ?A ?B)) (containsFormula ?TEXT (exists (?DAY) (and (weddingdate ?A ?B ?DAY) (instance ?DAY Day))))) |
Biography.kif 315-325 | If X is an instance of marriage certificate, Y is an instance of human, Z is an instance of human, and Y is the spouse of Z, then X contains the formula there exists W such that Y, Z were married on W, and W is an instance of day |
| (=> (instance ?C CalendarText) (exists (?D) (and (instance ?D Day) (refers ?C ?D)))) |
ComputingBrands.kif 2295-2300 | If X is an instance of calendar, then there exists Y such that Y is an instance of day and X includes a reference to Y |
| (=> (and (equal ?FY (FiscalYearStartingFn ?PLACE ?YEAR)) (fiscalYearPeriod ?PLACE ?PERIOD) (instance ?FY ?PERIOD)) (exists (?DAY ?INST) (and (instance ?DAY Day) (starts ?DAY ?FY) (instance ?INST ?YEAR) (temporalPart ?DAY ?INST)))) |
Economy.kif 4086-4096 | If equal X, the fiscal year starting of Y, and Z, W is a fiscal year period of Y, and X is an instance of W, then there exist V, U such that V is an instance of day, V starts X, U is an instance of Z, and V is a part of U |
| (=> (dayPhone ?Number ?Agent) (exists (?Phone ?Hour ?Num) (and (phoneNumber ?Number ?Phone) (greaterThan ?Num 6) (lessThan ?Num 18) (holdsDuring (instance ?Hour (HourFn ?Num Day)) (exists (?T) (and (instance ?T Telephoning) (destination ?T ?Agent) (patient ?T ?Phone) (possesses ?Agent ?Phone) (modalAttribute (exists (?A) (and (instance ?A Answering) (subProcess ?A ?T) (agent ?A ?Agent))) Likely))))))) |
FinancialOntology.kif 3709-3729 | If X is a day phone of Y, then All of the following hold: (1) there exist Z, W (2) V such that Z is a phone number of Y (3) V is greater than 6 (4) V is less than 18 (5) there exists U such that U is an instance of telephoning (6) U ends up at X (7) Z is a patient of U (8) X possesses Z (9) the statement there exists T such that T is an instance of answering (10) T is a subprocess of U (11) X is an agent of T has the modal force of likely holds during W is an instance of the hour V |
| (=> (eveningPhone ?Number ?Agent) (exists (?Phone ?Hour ?Num) (and (phoneNumber ?Number ?Phone) (greaterThan ?Num 18) (lessThan ?Num 6) (holdsDuring (instance ?Hour (HourFn ?Num Day)) (exists (?T) (and (instance ?T Telephoning) (destination ?T ?Agent) (patient ?T ?Phone) (possesses ?Agent ?Phone) (modalAttribute (exists (?A) (and (instance ?A Answering) (subProcess ?A ?T) (agent ?A ?Agent))) Likely))))))) |
FinancialOntology.kif 3753-3773 | If X is an evening phone of Y, then All of the following hold: (1) there exist Z, W (2) V such that Z is a phone number of Y (3) V is greater than 18 (4) V is less than 6 (5) there exists U such that U is an instance of telephoning (6) U ends up at X (7) Z is a patient of U (8) X possesses Z (9) the statement there exists T such that T is an instance of answering (10) T is a subprocess of U (11) X is an agent of T has the modal force of likely holds during W is an instance of the hour V |
| (=> (and (instance ?REGION GeographicArea) (located ?REGION ArcticRegion)) (exists (?DAY) (and (instance ?DAY Day) (holdsDuring ?DAY (not (attribute ?REGION Illuminated)))))) |
Geography.kif 5025-5034 | If X is an instance of geographic area and X is located at arctic region, then there exists Y such that Y is an instance of day and illuminated is not an attribute of X holds during Y |
| (=> (and (instance ?REGION GeographicArea) (located ?REGION AntarcticArea)) (exists (?DAY) (and (instance ?DAY Day) (holdsDuring ?DAY (not (attribute ?REGION Illuminated)))))) |
Geography.kif 5088-5097 | If X is an instance of geographic area and X is located at antarctic area, then there exists Y such that Y is an instance of day and illuminated is not an attribute of X holds during Y |
| (=> (and (instance ?POLICY DailyHousekeepingPolicy) (policyOwner ?AGENT ?POLICY)) (modalAttribute (exists (?GUEST ?ROOM ?STAY) (and (guest ?GUEST ?AGENT) (stays ?GUEST ?ROOM) (equal ?STAY (WhenFn (stays ?GUEST ?ROOM))) (holdsDuring ?STAY (forall (?DAY) (=> (and (instance ?DAY Day) (during ?DAY ?STAY)) (exists (?RC) (and (instance ?RC RoomCleaningService) (patient ?RC ?ROOM) (during ?RC ?DAY)))))))) Likely)) |
Hotel.kif 2665-2685 | If X is an instance of daily housekeeping and Y enacts policy X, then All of the following hold: (1) the statement there exist Z, W (2) V such that Z is a guest at Y (3) Z stays at W (4) equal V (5) the time of existence of Z stays at W (6) U U is an instance of day (7) U takes place during Vthere exists T such that T is an instance of service (8) W is a patient of T (9) T takes place during U holds during V has the modal force of likely |
| (=> (instance ?M Midnight) (exists (?D) (and (instance ?D Day) (equal ?M (EndFn ?D))))) |
Merge.kif 8914-8919 | If X is an instance of midnight, then there exists Y such that Y is an instance of day, equal X, and the end of Y |
| (=> (and (instance ?MONTH Month) (duration ?MONTH (MeasureFn ?NUMBER DayDuration))) (equal (CardinalityFn (TemporalCompositionFn ?MONTH Day)) ?NUMBER)) |
Merge.kif 9619-9623 | If X is an instance of month and duration of X is Y day duration(s), then equal the number of instances in decomposition of X into days and Y |
| (=> (instance ?WEEK Week) (equal (CardinalityFn (TemporalCompositionFn ?WEEK Day)) 7)) |
Merge.kif 9625-9627 | If X is an instance of week, then equal the number of instances in decomposition of X into days and 7 |
| (=> (and (instance ?WED Wedding) (date ?WED ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?CLASS ?FUTURE) (and (weddingAnniversary ?WED ?CLASS) (subclass ?CLASS Day) (instance ?FUTURE Integer) (equal ?CLASS (DayFn ?D (MonthFn ?M (YearFn ?FUTURE)))) (greaterThan ?FUTURE ?Y)))) |
Mid-level-ontology.kif 26561-26572 | 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 |
| (=> (and (birthdate ?A ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?CLASS ?FUTURE) (and (birthday ?A ?CLASS) (subclass ?CLASS Day) (instance ?FUTURE Integer) (equal ?CLASS (DayFn ?D (MonthFn ?M (YearFn ?FUTURE)))) (greaterThan ?FUTURE ?Y)))) |
Mid-level-ontology.kif 26602-26612 | 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 |
|
|
|