consequent

(=>     (instance ?M Midnight)     (exists (?D)         (and             (instance ?D Day)             (equal ?M                 (EndFn ?D)))))	Merge.kif 8983-8988	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 9688-9692	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 9694-9696	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 26479-26490	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 26520-26530	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
(=>     (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
(=>     (and         (instance ?REGION GeographicArea)         (located ?REGION ArcticRegion))     (exists (?DAY)         (and             (instance ?DAY Day)             (holdsDuring ?DAY                 (not                     (attribute ?REGION Illuminated))))))	Geography.kif 4996-5005	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 5059-5068	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

Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree

---

Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners