| appearance as argument number 1 |
|
| (documentation WhenFn ChineseLanguage "这是一个 UnaryFunction，它把一个 Object 或 Process 联系到它存在的准确 TimeInterval。注：在 TimeInterval (WhenFn ?THING)以外的 每一个 TimePoint ?TIME， (time ?THING ?TIME) 并不存在") | chinese_format.kif 2736-2738 | |
| (documentation WhenFn EnglishLanguage "A UnaryFunction that maps an Object or Process to the exact TimeInterval during which it exists. Note that, for every TimePoint ?TIME outside of the TimeInterval (WhenFn ?THING), (time ?THING ?TIME) does not hold.") | Merge.kif 8373-8376 | |
| (domain WhenFn 1 Physical) | Merge.kif 8370-8370 | 何时函数 的 1 数量 是 物理 的 instance |
| (instance WhenFn TemporalRelation) | Merge.kif 8367-8367 | 何时函数 是 时间关系 的 instance |
| (instance WhenFn TotalValuedRelation) | Merge.kif 8369-8369 | 何时函数 是 总值关系 的 instance |
| (instance WhenFn UnaryFunction) | Merge.kif 8368-8368 | 何时函数 是 一元函数 的 instance |
| (range WhenFn TimeInterval) | Merge.kif 8371-8371 | 何时函数 的 range 是 时距 的实例 |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage WhenFn "%1 出现 的 time") | chinese_format.kif 455-455 | |
| (format EnglishLanguage WhenFn "the time of existence of %1") | english_format.kif 461-461 | |
| (relatedInternalConcept WhereFn WhenFn) | Merge.kif 4135-4135 | 表示位置的函数 和 何时函数 是 内部相关 |
| (termFormat ChineseLanguage WhenFn "何时") | domainEnglishFormat.kif 62952-62952 | |
| (termFormat ChineseLanguage WhenFn "何时函数") | chinese_format.kif 456-456 | |
| (termFormat ChineseTraditionalLanguage WhenFn "何時") | domainEnglishFormat.kif 62951-62951 | |
| (termFormat EnglishLanguage WhenFn "when") | domainEnglishFormat.kif 62950-62950 |
| antecedent |
|
|
| consequent |
|
|
| (<=> (and (instance ?COMBINE Combining) (resource ?COMBINE ?OBJ1) (result ?COMBINE ?OBJ2)) (and (holdsDuring (BeginFn (WhenFn ?COMBINE)) (not (part ?OBJ1 ?OBJ2))) (holdsDuring (EndFn (WhenFn ?COMBINE)) (part ?OBJ1 ?OBJ2)))) |
Merge.kif 12228-12235 | 过程 是 结合 的 instance 和 客体 是 那个 过程 的 resource 和 实体 是 那个 过程 的 result 若且唯若 那个 客体 不 是 那个 实体 的 part 在 那个 过程 出现 的 time 的开始 holdsDuring 和 那个 客体 是 那个 实体 的 part 在 那个 过程 出现 的 time 的结束 holdsDuring |
| (<=> (and (instance ?Y (YearFn ?YEAR)) (equal (MaleLifeExpectancyAtBirthFn ?AREA ?Y) ?REALNUMBER)) (exists (?LIST) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (attribute ?INDIVIDUAL Male) (during (WhenFn ?BIRTH) ?Y) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER)))) |
People.kif 372-405 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 另一个 整数 的 instance 和 对所有 那个 串列ITEM
|
| (<=> (equal (BirthsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (DivisionFn (PopulationFn ?AREA) 1000) ?THOUSANDS) (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 108-121 | 地缘政治区域 和 整数 year 每一千的 births equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
| (<=> (equal (DeathsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (DivisionFn (PopulationFn ?AREA) 1000) ?THOUSANDS) (equal ?DEATHCOUNT (CardinalityFn (KappaFn ?DEATH (and (instance ?DEATH Death) (experiencer ?DEATH ?PERSON) (instance ?PERSON Human) (during (WhenFn ?DEATH) (YearFn ?YEAR)) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?DEATHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 142-155 | 地缘政治区域 和 整数 year 每一千里的 deaths equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
| (<=> (equal (DeathsPerThousandLiveBirthsFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT 1000) ?THOUSANDSOFBIRTHS) (equal ?INFANTDEATHCOUNT (CardinalityFn (KappaFn ?DEATH (and (instance ?DEATH Death) (experiencer ?DEATH ?INFANT) (instance ?INFANT Human) (age ?INFANT (MeasureFn ?AGE YearDuration)) (lessThan ?AGE 1) (during (WhenFn ?DEATH) (YearFn ?YEAR)) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?INFANTDEATHCOUNT ?THOUSANDSOFBIRTHS) ?REALNUMBER))) |
People.kif 257-281 | 地缘政治区域 和 整数 year 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
| (<=> (equal (FemaleLifeExpectancyAtBirthFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (exists (?LIST) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (attribute ?INDIVIDUAL Female) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER)))) |
People.kif 418-449 | 地缘政治区域 和 整数 year 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 另一个 整数 的 instance 和 对所有 那个 串列ITEM
|
| (<=> (equal (LifeExpectancyAtBirthFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (exists (?LIST) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER)))) |
People.kif 327-357 | 地缘政治区域 和 整数 year 的出生预期 life equal 实数 若且唯若 有存在 串列 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 另一个 整数 的 instance 和 对所有 那个 串列ITEM
|
| (<=> (holdsDuring ?T (attribute ?H Alone)) (not (exists (?H2 ?SI) (and (not (equal ?H ?H2)) (instance ?H2 Agent) (instance ?SI SocialInteraction) (during (WhenFn ?SI) ?T) (involvedInEvent ?SI ?H) (involvedInEvent ?SI ?H2))))) |
Mid-level-ontology.kif 29621-29634 | Alone 是 实体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 那个 实体2 和 过程 这样 那个 实体 不 equal 那个 实体2 和 那个 实体2 是 施事体 的 instance 和 那个 过程 是 社交 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 实体 是事件 那个 过程 的 involved 和 那个 实体2 是事件 那个 过程 的 involved |
| (<=> (holdsDuring ?T (attribute ?P Mute)) (not (exists (?S) (and (instance ?S Speaking) (during (WhenFn ?S) ?T) (agent ?S ?P))))) |
Mid-level-ontology.kif 29669-29677 | Mute 是 施事体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 过程 这样 那个 过程 是 说话 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 施事体 是 那个 过程 的 agent |
| (=> (almaMater ?PERSON ?SCHOOL) (exists (?EV) (and (instance ?EV EducationalProcess) (destination ?EV ?PERSON) (eventLocated ?EV ?SCHOOL) (holdsDuring (WhenFn ?EV) (attribute ?PERSON Student))))) |
Mid-level-ontology.kif 16291-16300 | |
| (=> (and (actedIn ?ACTOR ?O) (instance ?PERF DramaticActing) (patient ?PERF ?ACTOR) (result ?PERF ?O)) (holdsDuring (WhenFn ?PERF) (attribute ?ACTOR Actor))) |
Mid-level-ontology.kif 20097-20104 | |
| (=> (and (agent ?PROCESS ?AGENT) (result ?PROCESS ?WORK) (instance ?WORK ArtWork)) (holdsDuring (WhenFn ?PROCESS) (attribute ?AGENT Artist))) |
Mid-level-ontology.kif 18208-18214 | |
| (=> (and (allergic ?H ?S) (instance ?SUB ?S) (holdsDuring ?T (meetsSpatially ?S ?H))) (modalAttribute (exists (?AR) (and (instance ?AR AllergicReaction) (experiencer ?AR ?H) (overlapsTemporally ?T (WhenFn ?AR)) (before (BeginFn ?T) (BeginFn (WhenFn ?AR))))) Likely)) |
Mid-level-ontology.kif 5907-5920 | |
| (=> (and (attribute ?AC TwoFactorAuthentication) (loggedInDuring ?A ?AC ?T)) (exists (?TF) (and (instance ?TF TwoFactorLoggingIn) (agent ?TF ?A) (accountUsed ?TF ?AC) (earlier (WhenFn ?TF) ?T)))) |
ComputingBrands.kif 4336-4345 | |
| (=> (and (attribute ?H Muslim) (equal (WealthFn ?H) ?W)) (modalAttribute (exists (?Z ?T ?U) (and (instance ?Z Zakat) (instance ?Y Year) (during ?Y (WhenFn ?H)) (holdsDuring ?Y (attribute ?H FullyFormed)) (agent ?Z ?H) (patient ?Z ?T) (monetaryValue ?T (MeasureFn ?C ?U)) (instance ?U UnitOfCurrency) (greaterThan ?C (MultiplicationFn ?W 0.025)))) Obligation)) |
ArabicCulture.kif 193-212 |
|
| (=> (and (attribute ?MR CoverRecording) (instance ?MR MusicRecording) (songArtist ?MR ?A) (musicInterpretation ?MR ?M) (record ?MR ?MM)) (exists (?ORIG ?ARTIST ?MUSIC) (and (musicInterpretation ?ORIG ?M) (songArtist ?ORIG ?ARTIST) (not (equal ?A ?ARTIST)) (record ?ORIG ?MUSIC) (before (WhenFn ?MUSIC) (WhenFn ?MM))))) |
Music.kif 455-468 |
|
| (=> (and (attribute ?Order FOKOrder) (agreementPeriod ?Order ?Period)) (or (exists (?Fill ?Time1) (and (instance ?Fill FillingAnOrder) (patient ?Fill ?Order) (equal (WhenFn ?Fill) ?Time1) (starts ?Time1 ?Period))) (exists (?Kill ?Time2) (and (instance ?Kill CancellingAnOrder) (patient ?Kill ?Order) (equal (WhenFn ?Kill) ?Time2) (starts ?Time2 ?Period))))) |
FinancialOntology.kif 2888-2904 |
|
| (=> (and (attribute ?Order GTCOrder) (agreementPeriod ?Order ?Period)) (or (exists (?Execute) (and (instance ?Execute FillingAnOrder) (patient ?Execute ?Order) (equal (WhenFn ?Execute) ?Time) (overlapsTemporally ?Time ?Period))) (exists (?Cancel) (and (instance ?Cancel CancellingAnOrder) (patient ?Cancel ?Order) (equal (WhenFn ?Cancel) ?End) (finishes ?End ?Period))))) |
FinancialOntology.kif 2924-2940 |
|
| (=> (and (attribute ?Order IOCOrder) (agreementPeriod ?Order ?Period)) (or (exists (?Fill ?Time1) (and (instance ?Fill FillingAnOrder) (patient ?Fill ?Order) (equal (WhenFn ?Fill) ?Time1) (starts ?Time1 ?Period))) (exists (?Kill ?Time2) (and (instance ?Kill CancellingAnOrder) (patient ?Kill ?Order) (equal (WhenFn ?Kill) ?Time2) (starts ?Time2 ?Period))))) |
FinancialOntology.kif 2861-2877 |
|
| (=> (and (attribute ?Order LimitOrder) (partyToAgreement ?Order ?Broker) (attribute ?Broker Broker) (orderFor ?Order Buying ?Object) (measure ?Object ?Quantity) (limitPrice ?Order (MeasureFn ?LimitPrice ?U)) (instance ?U UnitOfCurrency) (askPrice ?Object (MeasureFn ?Price ?U) ?Time) (lessThanOrEqualTo ?Price ?LimitPrice)) (holdsObligation (KappaFn ?Buy (and (instance ?Buy Buying) (patient ?Buy ?Object) (measure ?Object ?Quantity) (equal (WhenFn ?Buy) ?BuyingTime) (overlapsTemporally ?Time ?BuyingTime))) ?Broker)) |
FinancialOntology.kif 2017-2038 |
|
| (=> (and (attribute ?Order LimitOrder) (partyToAgreement ?Order ?Broker) (attribute ?Broker Broker) (orderFor ?Order Selling ?Object) (measure ?Object ?Quantity) (limitPrice ?Order (MeasureFn ?LimitPrice ?U)) (bidPrice ?Object (MeasureFn ?Price ?U) ?Time) (instance ?U UnitOfCurrency) (greaterThanOrEqualTo ?Price ?LimitPrice)) (holdsObligation (KappaFn ?Sell (and (instance ?Sell Selling) (patient ?Sell ?Object) (measure ?Object ?Quantity) (equal (WhenFn ?Sell) ?SellingTime) (overlapsTemporally ?SellingTime ?Time))) ?Broker)) |
FinancialOntology.kif 2040-2061 |
|
| (=> (and (attribute ?X CommunalAttribute) (instance ?X Table) (instance ?E1 Eating) (agent ?E1 ?GRP1) (instance ?GRP1 GroupOfPeople) (eventLocated ?E1 ?X)) (modalAttribute (exists (?GRP2 ?E2) (and (instance ?E2 Eating) (agent ?E2 ?GRP2) (not (equal ?GRP1 ?GRP2)) (instance ?GRP2 GroupOfPeople) (eventLocated ?E2 ?X2) (meetsTemporally (WhenFn ?E1) (WhenFn ?E2)) (equal ?X ?X2))) Possibility)) |
Dining.kif 1160-1177 |
|
| (=> (and (boilingPoint ?TYPE (MeasureFn ?TEMP1 ?MEASURE)) (instance ?SUBSTANCE ?TYPE) (holdsDuring ?TIME (measure ?SUBSTANCE (MeasureFn ?TEMP2 ?MEASURE))) (instance ?MEASURE UnitOfTemperature) (greaterThanOrEqualTo ?TEMP2 ?TEMP1)) (or (holdsDuring ?TIME (attribute ?SUBSTANCE Gas)) (exists (?BOIL) (and (overlapsTemporally (WhenFn ?BOIL) ?TIME) (instance ?BOIL Boiling) (patient ?BOIL ?SUBSTANCE))))) |
Merge.kif 13595-13608 |
|
| (=> (and (checkOutTime ?HOTEL ?TIME) (guest ?GUEST ?HOTEL)) (expects ?HOTEL (exists (?T ?C) (and (instance ?T ?TIME) (patient ?C ?GUEST) (instance ?C CheckOutService) (agent ?C ?HOTEL) (before (BeginFn (WhenFn ?C)) ?T))))) |
Hotel.kif 663-674 | |
| (=> (and (destination ?MSG ?TELEX) (instance ?MSG Messaging) (patient ?MSG ?M) (instance ?TELEX Telex)) (exists (?PROC ?TEXT) (and (instrument ?PROC ?TELEX) (result ?PROC ?TEXT) (represents ?TEXT ?M) (instance ?TEXT Text) (before (BeginFn (WhenFn ?MSG)) (BeginFn (WhenFn ?PROC)))))) |
Communications.kif 202-214 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| (exists (?TIME) (and (instance ?TIME TimeInterval) (finishes ?TIME (WhenFn JesusOfNazareth)) (starts ?TIME (WhenFn TwelveApostles)) (forall (?MEM) (=> (holdsDuring ?TIME (member ?MEM TwelveApostles)) (holdsDuring ?TIME (friend ?MEM JesusOfNazareth)))))) |
Media.kif 1968-1976 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|
| (holdsDuring (WhenFn JesusOfNazareth) (located JesusOfNazareth Palestine)) |
Media.kif 1918-1918 | JesusOfNazareth 是 located 在 巴勒斯坦 在 JesusOfNazareth 出现 的 time holdsDuring |
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners