Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| Advent(advent) |  | Advent |
| appearance as argument number 1 |
|
|
| (subclass Advent ChristianHoliday) | Media.kif 290-290 | Advent is a subclass of Christian holiday |
| (subclass Advent MoveableHoliday) | Media.kif 291-291 | Advent is a subclass of moveable holiday |
| (documentation Advent EnglishLanguage "An instance of Advent (LatinLanguage adventus = coming) is a TimeInterval that begins with an AdventSunday and includes the four Sundays preceding an instance of ChristmasDay. During this period, observant members of Christianity ritually anticipate the recurring celebration of the birth of Jesus of Nazareth. Note that Advent is observed only in Western Christianity, which includes RomanCatholicism, Protestantism, and Anglicanism. The analog of Advent in Eastern Christianity, which includes EasternOrthodoxChristianity, is the Nativity Fast, which differs from Advent in length and significance.") | Media.kif 292-302 | Advent is a subclass of moveable holiday |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage Advent "advent") | domainEnglishFormat.kif 64411-64411 |
| antecedent |
|
|
| (=> (instance ?T1 Advent) (exists (?T2) (and (instance ?T2 AdventSunday) (starts ?T2 ?T1)))) |
Media.kif 311-316 | If X is an instance of advent, then there exists Y such that Y is an instance of advent sunday and Y starts X |
| (=> (instance ?T1 Advent) (exists (?T2) (and (instance ?T2 ChristmasDay) (meetsTemporally ?T1 ?T2)))) |
Media.kif 363-368 | If X is an instance of advent, then there exists Y such that Y is an instance of Christmas day and X meets Y |
| (=> (and (instance ?T1 Advent) (instance ?T2 ChristmasDay) (meetsTemporally ?T1 ?T2)) (exists (?YEAR) (and (instance ?YEAR Year) (during ?T1 ?YEAR) (during ?T2 ?YEAR)))) |
Media.kif 370-379 | If X is an instance of advent, Y is an instance of Christmas day, and X meets Y, then there exists Z such that Z is an instance of year, X takes place during Z, and Y takes place during Z |
| (=> (and (instance ?T1 Advent) (instance ?T2 ChristmasDay) (during ?T1 ?YEAR) (instance ?YEAR Year) (meetsTemporally ?T1 ?T2)) (during ?T2 ?YEAR)) |
Media.kif 381-388 | If X is an instance of advent, Y is an instance of Christmas day, X takes place during Z, Z is an instance of year, and X meets Y, then Y takes place during Z |
| (=> (and (instance ?T1 Advent) (instance ?T2 ChristmasDay) (during ?T2 ?YEAR) (instance ?YEAR Year) (meetsTemporally ?T1 ?T2)) (during ?T1 ?YEAR)) |
Media.kif 390-397 | If X is an instance of advent, Y is an instance of Christmas day, Y takes place during Z, Z is an instance of year, and X meets Y, then X takes place during Z |
| consequent |
|
|
| (=> (instance ?T1 AdventSunday) (exists (?T2) (and (instance ?T2 Advent) (starts ?T1 ?T2)))) |
Media.kif 321-326 | If X is an instance of advent sunday, then there exists Y such that Y is an instance of advent and X starts Y |
| (=> (instance ?T1 ChristmasDay) (exists (?T2) (and (instance ?T2 Advent) (meetsTemporally ?T2 ?T1)))) |
Media.kif 356-361 | If X is an instance of Christmas day, then there exists Y such that Y is an instance of advent and Y meets X |
|