Browsing Interface : Welcome guest : log in		 [  Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - TimeInterval
TimeInterval(时距)

appearance as argument number 1
-------------------------


(documentation TimeInterval ChineseLanguage "这是一个时段。注： TimeInterval 在通用时间轴上 皆有范围和位置；另外 TimeInterval 是没有间隙的，即这个类别只含凸时间间隔。") chinese_format.kif 1785-1786
(documentation TimeInterval EnglishLanguage "An interval of time. Note that a TimeInterval has both an extent and a location on the universal timeline. Note too that a TimeInterval has no gaps, i.e. this class contains only convex time intervals.") Merge.kif 1999-2002
(subclass TimeInterval TimePosition) Merge.kif 1997-1997 时距 是 时间位置 的 subclass

appearance as argument number 2
-------------------------


(instance BeforeCommonEra TimeInterval) Mid-level-ontology.kif 7568-7568 共同的时代之前 是 时距 的 instance
(instance CommonEra TimeInterval) Mid-level-ontology.kif 7576-7576 共同时代 是 时距 的 instance
(partition TimePosition TimeInterval TimePoint) Merge.kif 1992-1992 时间位置 详尽无遗地 partition 成 时距 和 时点
(range FiscalYearStartingFn TimeInterval) Economy.kif 3727-3727 财政年度开始 的 range 是 时距 的实例
(range FutureFn TimeInterval) Merge.kif 7985-7985 未来函数 的 range 是 时距 的实例
(range ImmediateFutureFn TimeInterval) Merge.kif 8002-8002 紧接未来函数 的 range 是 时距 的实例
(range ImmediatePastFn TimeInterval) Merge.kif 7971-7971 紧接过去函数 的 range 是 时距 的实例
(range PastFn TimeInterval) Merge.kif 7953-7953 过去函数 的 range 是 时距 的实例
(range SiteSpeedFn TimeInterval) UXExperimentalTerms.kif 3953-3953 SiteSpeedFn 的 range 是 时距 的实例
(range TTFxFn TimeInterval) UXExperimentalTerms.kif 1700-1700 TTFxFn 的 range 是 时距 的实例
(range TimeIntervalFn TimeInterval) Merge.kif 7886-7886 时段函数 的 range 是 时距 的实例
(range TimePeriodFn TimeInterval) Mid-level-ontology.kif 11674-11674 TimePeriodFn 的 range 是 时距 的实例
(range WhenFn TimeInterval) Merge.kif 7942-7942 何时函数 的 range 是 时距 的实例
(rangeSubclass FiscalYearFn TimeInterval) Economy.kif 3701-3701 财政年度 的所得值 是 时距 的 subclass
(rangeSubclass RecurrentTimeIntervalFn TimeInterval) Merge.kif 7919-7919 重复发生时间函数 的所得值 是 时距 的 subclass
(rangeSubclass TemporalCompositionFn TimeInterval) Merge.kif 8833-8833 时间分拆函数 的所得值 是 时距 的 subclass
(subclass AnteMeridiem TimeInterval) Mid-level-ontology.kif 16907-16907 上午 是 时距 的 subclass
(subclass BreakfastTime TimeInterval) Food.kif 195-195 BreakfastTime 是 时距 的 subclass
(subclass Day TimeInterval) Merge.kif 8688-8688 日 是 时距 的 subclass
(subclass DayTime TimeInterval) Merge.kif 8323-8323 一天的时间 是 时距 的 subclass
(subclass Decade TimeInterval) Merge.kif 8239-8239 Decade 是 时距 的 subclass
(subclass DhuAlHijjah TimeInterval) ArabicCulture.kif 103-103 Dhu al hijjah 是 时距 的 subclass
(subclass DinnerTime TimeInterval) Food.kif 224-224 DinnerTime 是 时距 的 subclass
(subclass Holiday TimeInterval) Mid-level-ontology.kif 12579-12579 假日 是 时距 的 subclass
(subclass Hour TimeInterval) Merge.kif 8798-8798 小时 是 时距 的 subclass

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

appearance as argument number 3
-------------------------


(domain BeginFn 1 TimeInterval) Merge.kif 7581-7581 开始函数 的 1 数量 是 时距 的 instance
(domain EndFn 1 TimeInterval) Merge.kif 7609-7609 结束函数 的 1 数量 是 时距 的 instance
(domain GPIFn 2 TimeInterval) UXExperimentalTerms.kif 3364-3364 GPIFn 的 2 数量 是 时距 的 instance
(domain MusicalInterpretationFn 3 TimeInterval) Music.kif 843-843 MusicalInterpretationFn 的 3 数量 是 时距 的 instance
(domain PPIFn 2 TimeInterval) UXExperimentalTerms.kif 3290-3290 PPIFn 的 2 数量 是 时距 的 instance
(domain SCRFn 2 TimeInterval) UXExperimentalTerms.kif 3865-3865 SCRFn 的 2 数量 是 时距 的 instance
(domain SiteWideNewBuyersFn 1 TimeInterval) UXExperimentalTerms.kif 3569-3569 SiteWideNewBuyersFn 的 1 数量 是 时距 的 instance
(domain SiteWideNewRegistrationsFn 1 TimeInterval) UXExperimentalTerms.kif 3621-3621 SiteWideNewRegistrationsFn 的 1 数量 是 时距 的 instance
(domain SiteWideNewSellersFn 1 TimeInterval) UXExperimentalTerms.kif 3668-3668 SiteWideNewSellersFn 的 1 数量 是 时距 的 instance
(domain TemporalCompositionFn 1 TimeInterval) Merge.kif 8831-8831 时间分拆函数 的 1 数量 是 时距 的 instance
(domain agreementPeriod 2 TimeInterval) Mid-level-ontology.kif 11647-11647 协议期限 的 2 数量 是 时距 的 instance
(domain anniversary 2 TimeInterval) Mid-level-ontology.kif 21986-21986 周年 的 2 数量 是 时距 的 instance
(domain burnInPeriod 2 TimeInterval) UXExperimentalTerms.kif 4506-4506 burnInPeriod 的 2 数量 是 时距 的 instance
(domain compoundInterest 3 TimeInterval) FinancialOntology.kif 525-525 复利 的 3 数量 是 时距 的 instance
(domain constructionPeriod 2 TimeInterval) Mid-level-ontology.kif 18489-18489 constructionPeriod 的 2 数量 是 时距 的 instance
(domain creditsPerPeriod 3 TimeInterval) FinancialOntology.kif 3714-3714 每期积分 的 3 数量 是 时距 的 instance
(domain daylightHoursInterval 3 TimeInterval) Weather.kif 463-463 白天小时间隔 的 3 数量 是 时距 的 instance
(domain duration 1 TimeInterval) Merge.kif 7508-7508 时段 的 1 数量 是 时距 的 instance
(domain during 1 TimeInterval) Merge.kif 7807-7807 在这时间内 的 1 数量 是 时距 的 instance
(domain during 2 TimeInterval) Merge.kif 7808-7808 在这时间内 的 2 数量 是 时距 的 instance
(domain earlier 1 TimeInterval) Merge.kif 7852-7852 更早 的 1 数量 是 时距 的 instance
(domain earlier 2 TimeInterval) Merge.kif 7853-7853 更早 的 2 数量 是 时距 的 instance
(domain employeeContribution 3 TimeInterval) FinancialOntology.kif 3248-3248 员工贡献 的 3 数量 是 时距 的 instance
(domain finishes 1 TimeInterval) Merge.kif 7658-7658 完成 的 1 数量 是 时距 的 instance
(domain finishes 2 TimeInterval) Merge.kif 7659-7659 完成 的 2 数量 是 时距 的 instance

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

antecedent
-------------------------


(=>
    (and
        (holdsDuring ?T1
            (and
                (attribute ?P Expellee)
                (citizen ?P ?HOME-NATION)))
        (instance ?T1 TimeInterval))
    (exists (?TRANS ?NATION)
        (and
            (instance ?NATION Nation)
            (not
                (equal ?NATION ?HOME-NATION))
            (instance ?TRANS Translocation)
            (origin ?TRANS ?NATION)
            (patient ?TRANS ?P)
            (destination ?TRANS ?HOME-NATION)
            (temporalPart ?T1
                (WhenFn ?TRANS)))))		 MilitaryPersons.kif 151-167
(=>
    (and
        (holdsDuring ?T1
            (and
                (attribute ?PERSON DislocatedCivilian)
                (inhabits ?PERSON ?RESIDENCE)
                (located ?RESIDENCE ?PLACE)))
        (instance ?PLACE GeographicArea)
        (instance ?T1 TimeInterval))
    (exists (?T0 ?PRIOR-PLACE ?PRIOR-RES)
        (and
            (instance ?T0 TimeInterval)
            (earlier ?T0 ?T1)
            (instance ?PRIOR-RES Object)
            (instance ?PRIOR-PLACE GeopoliticalArea)
            (located ?PRIOR-RES ?PRIOR-PLACE)
            (not
                (equal ?PLACE ?PRIOR-PLACE))
            (not
                (equal ?RESIDENCE ?PRIOR-RES))
            (not
                (geographicSubregion ?PLACE ?PRIOR-PLACE))
            (not
                (geographicSubregion ?PRIOR-PLACE ?PLACE))
            (holdsDuring ?T0
                (inhabits ?PERSON ?PRIOR-RES)))))		 MilitaryPersons.kif 26-47
(=>
    (and
        (holdsDuring ?T1
            (attribute ?P Evacuee))
        (instance ?T1 TimeInterval))
    (exists (?EV ?MIL)
        (and
            (instance ?EV Evacuation)
            (agent ?EV ?MIL)
            (instance ?MIL MilitaryOrganization)
            (experiencer ?EV ?P)
            (earlier
                (WhenFn ?EV) ?T1))))		 MilitaryPersons.kif 120-131
(=>
    (and
        (holdsDuring ?T1
            (attribute ?P InternallyDisplacedPerson))
        (instance ?T1 TimeInterval))
    (exists (?SITUATION)
        (and
            (earlier ?T0 ?T1)
            (causesProposition
                (holdsDuring ?T0
                    (fears ?P ?SITUATION))
                (holdsDuring ?T1
                    (attribute ?P InternallyDisplacedPerson))))))		 MilitaryPersons.kif 101-111
(=>
    (and
        (holdsDuring ?T1
            (spouse ?P1 ?P2))
        (instance ?T1 TimeInterval))
    (exists (?WED)
        (and
            (instance ?WED Wedding)
            (patient ?WED ?P1)
            (patient ?WED ?P2)
            (earlier
                (WhenFn ?WED) ?T1))))		 Mid-level-ontology.kif 7639-7649
(=>
    (and
        (holdsDuring ?T2 ?SIT2)
        (holdsDuring ?T1 ?SIT1)
        (instance ?T1 TimeInterval)
        (instance ?T2 TimeInterval)
        (causesProposition ?SIT1 ?SIT2))
    (beforeOrEqual
        (BeginFn ?T1)
        (BeginFn ?T2)))		 Merge.kif 3700-3707
(=>
    (and
        (instance ?ACCESSING AccessingWebPage)
        (instance ?PAGE WebPage)
        (instance ?TRANSFER DataTransfer)
        (instance ?SERVER Server)
        (instance ?REQUESTING Requesting)
        (instance ?BROWSER WebBrowser)
        (instance ?INTERVAL TimeInterval)
        (patient ?ACCESSING ?PAGE)
        (agent ?REQUESTING ?BROWSER)
        (destination ?REQUESTING ?SERVER)
        (patient ?REQUESTING ?PAGE)
        (origin ?TRANSFER ?SERVER)
        (destination ?TRANSFER ?BROWSER)
        (patient ?TRANSFER ?PAGE)
        (subProcess ?TRANSFER ?ACCESSING)
        (subProcess ?REQUESTING ?ACCESSING)
        (equal
            (EndFn
                (WhenFn ?REQUESTING))
            (BeginFn ?INTERVAL))
        (equal
            (EndFn
                (WhenFn ?TRANSFER))
            (EndFn ?INTERVAL)))
    (equal
        (SiteSpeedFn ?ACCESSING) ?INTERVAL))		 UXExperimentalTerms.kif 3963-3988
(=>
    (and
        (instance ?EXPERIMENT Experimenting)
        (instance ?INTERVAL TimeInterval))
    (equal
        (DivisionFn
            (CardinalityFn
                (KappaFn ?PURCHASE
                    (and
                        (instance ?PURCHASE Buying)
                        (member ?PURCHASE
                            (QualifyingPurchasesFn ?EXPERIMENT))
                        (during
                            (WhenFn ?PURCHASE) ?INTERVAL))))
            (CardinalityFn
                (KappaFn ?USER
                    (and
                        (member ?USER
                            (TreatedUsersFn ?EXPERIMENT))
                        (instance ?ACCESSING AccessingWebPage)
                        (during
                            (WhenFn ?ACCESSING) ?INTERVAL)
                        (agent ?ACCESSING ?USER)))))
        (PPIFn ?EXPERIMENT ?INTERVAL)))		 UXExperimentalTerms.kif 3299-3318
(=>
    (and
        (instance ?EXPERIMENT Experimenting)
        (instance ?INTERVAL TimeInterval))
    (equal
        (DivisionFn
            (CardinalityFn
                (KappaFn ?PURCHASE
                    (and
                        (instance ?PURCHASE Buying)
                        (member ?PURCHASE
                            (QualifyingPurchasesFn ?EXPERIMENT)))))
            (CardinalityFn
                (KappaFn ?USER
                    (and
                        (member ?USER
                            (TreatedUsersFn ?EXPERIMENT))
                        (instance ?ACCESSING AccessingWebPage)
                        (agent ?ACCESSING ?USER)))))
        (PPSFn ?EXPERIMENT)))		 UXExperimentalTerms.kif 3260-3277
(=>
    (and
        (instance ?IMPRISON Imprisoning)
        (detainee ?IMPRISON ?AGENT)
        (instance ?AGENT Human)
        (time ?IMPRISON ?INTERVAL)
        (instance ?INTERVAL TimeInterval))
    (exists (?ARREST ?TIME)
        (and
            (instance ?TIME TimeInterval)
            (time ?ARREST ?TIME)
            (earlier ?TIME ?INTERVAL)
            (instance ?ARREST PlacingUnderArrest)
            (arrested ?ARREST ?AGENT))))		 Mid-level-ontology.kif 21468-21481
(=>
    (and
        (instance ?INTERVAL TimeInterval)
        (instance ?SITE WebSite))
    (exists (?NEWBUYERS)
        (and
            (instance ?NEWBUYERS Collection)
            (forall (?AGENT)
                (=>
                    (member ?AGENT ?NEWBUYERS)
                    (and
                        (exists (?BUYING)
                            (and
                                (instance ?AGENT Agent)
                                (instance ?BUYING Buying)
                                (agent ?BUYING ?AGENT)
                                (instrument ?BUYING ?SITE)
                                (during ?BUYING ?INTERVAL)))
                        (not
                            (exists (?INTERVAL_BEFORE)
                                (and
                                    (instance ?INTERVAL_BEFORE TimeInterval)
                                    (earlier ?INTERVAL_BEFORE ?INTERVAL)
                                    (holdsDuring ?INTERVAL_BEFORE
                                        (exists (?BUYING_BEFORE)
                                            (and
                                                (instance ?BUYING_BEFORE Buying)
                                                (agent ?BUYING_BEFORE ?AGENT)
                                                (instrument ?BUYING_BEFORE ?SITE)
                                                (during ?BUYING_BEFORE ?INTERVAL))))))))))
            (equal
                (SiteWideNewBuyersFn ?INTERVAL ?SITE) ?NEWBUYERS))))		 UXExperimentalTerms.kif 3581-3613
(=>
    (and
        (instance ?INTERVAL TimeInterval)
        (instance ?SITE WebSite))
    (exists (?NEWREGISTRATIONS)
        (and
            (instance ?NEWREGISTRATIONS Collection)
            (forall (?USER)
                (=>
                    (and
                        (instance ?USER Human)
                        (not
                            (exists (?INTERVAL_BEFORE)
                                (and
                                    (instance ?INTERVAL_BEFORE TimeInterval)
                                    (earlier ?INTERVAL_BEFORE ?INTERVAL)
                                    (holdsDuring ?INTERVAL_BEFORE
                                        (registeredUser ?USER ?SITE)))))
                        (exists (?INTERVAL_DURING)
                            (and
                                (instance ?INTERVAL_DURING TimeInterval)
                                (during ?INTERVAL_DURING ?INTERVAL)
                                (holdsDuring ?INTERVAL
                                    (registeredUser ?USER ?SITE)))))
                    (member ?USER ?NEWREGISTRATIONS)))
            (equal ?NEWREGISTRATIONS
                (SiteWideNewRegistrationsFn ?INTERVAL ?SITE)))))		 UXExperimentalTerms.kif 3633-3660
(=>
    (and
        (instance ?INTERVAL TimeInterval)
        (instance ?SITE WebSite))
    (exists (?NEWSELLERS)
        (and
            (instance ?NEWSELLERS Collection)
            (forall (?AGENT)
                (=>
                    (member ?AGENT ?NEWSELLERS)
                    (and
                        (exists (?SELLING)
                            (and
                                (instance ?AGENT Agent)
                                (instance ?SELLING Selling)
                                (agent ?SELLING ?AGENT)
                                (instrument ?SELLING ?SITE)
                                (during ?SELLING ?INTERVAL)))
                        (not
                            (exists (?INTERVAL_BEFORE)
                                (and
                                    (instance ?INTERVAL_BEFORE TimeInterval)
                                    (earlier ?INTERVAL_BEFORE ?INTERVAL)
                                    (holdsDuring ?INTERVAL_BEFORE
                                        (exists (?SELLING_BEFORE)
                                            (and
                                                (instance ?SELLING_BEFORE Selling)
                                                (agent ?SELLING_BEFORE ?AGENT)
                                                (instrument ?SELLING_BEFORE ?SITE)
                                                (during ?SELLING_BEFORE ?INTERVAL))))))))))
            (equal
                (SiteWideNewSellersFn ?INTERVAL ?SITE) ?NEWSELLERS))))		 UXExperimentalTerms.kif 3680-3712
(=>
    (and
        (instance ?POINT1 TimePoint)
        (instance ?POINT2 TimePoint)
        (instance ?INTERVAL TimeInterval)
        (equal
            (TimeIntervalFn ?POINT1 ?POINT2) ?INTERVAL))
    (and
        (equal
            (BeginFn ?INTERVAL) ?POINT1)
        (equal
            (EndFn ?INTERVAL) ?POINT2)))		 Merge.kif 7893-7901
(=>
    (and
        (instance ?POINT1 TimePoint)
        (instance ?POINT2 TimePoint)
        (instance ?INTERVAL TimeInterval)
        (equal
            (TimeIntervalFn ?POINT1 ?POINT2) ?INTERVAL))
    (forall (?POINT)
        (<=>
            (temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
            (temporalPart ?POINT ?INTERVAL))))		 Merge.kif 7903-7912
(=>
    (and
        (instance ?PROCESS ?PROCESS_CLASS)
        (subclass ?PROCESS_CLASS Process)
        (instance ?ACCESSING AccessingWebPage)
        (instance ?AGENT Agent)
        (agent ?PROCESS ?AGENT)
        (agent ?ACCESSING ?AGENT)
        (during ?PROCESS ?ACCESSING)
        (instance ?TIMETOFIRST TimeInterval)
        (not
            (exists (?PROCESS2)
                (and
                    (instance ?PROCESS2 ?PROCESS_CLASS)
                    (agent ?PROCESS2 ?AGENT)
                    (during ?PROCESS2 ?ACCESSING)
                    (before
                        (BeginFn
                            (WhenFn ?PROCESS2))
                        (BeginFn
                            (WhenFn ?PROCESS))))))
        (equal
            (BeginFn
                (WhenFn ?ACCESSING))
            (BeginFn
                (WhenFn ?TIMETOFIRST)))
        (equal
            (BeginFn
                (WhenFn ?PROCESS))
            (EndFn
                (WhenFn ?TIMETOFIRST))))
    (equal
        (TTFxFn ?PROCESS_CLASS ?ACCESSING) ?TIMETOFIRST))		 UXExperimentalTerms.kif 1702-1724
(=>
    (and
        (instance ?YEAR TimeInterval)
        (holdsDuring ?YEAR
            (economyType ?AREA LowIncomeCountry)))
    (and
        (perCapitaGDPInPeriod ?AREA
            (MeasureFn ?AMOUNT UnitedStatesDollar) ?YEAR)
        (lessThan ?AMOUNT 756)))		 Economy.kif 440-446
(=>
    (and
        (instance ?YEAR TimeInterval)
        (holdsDuring ?YEAR
            (economyType ?AREA LowerMiddleIncomeCountry)))
    (and
        (perCapitaGDPInPeriod ?AREA
            (MeasureFn ?AMOUNT UnitedStatesDollar) ?YEAR)
        (greaterThanOrEqualTo ?AMOUNT 756)))		 Economy.kif 455-461
(=>
    (and
        (instance ?YEAR TimeInterval)
        (holdsDuring ?YEAR
            (economyType ?AREA LowerMiddleIncomeCountry)))
    (and
        (perCapitaGDPInPeriod ?AREA
            (MeasureFn ?AMOUNT UnitedStatesDollar) ?YEAR)
        (lessThan ?AMOUNT 2996)))		 Economy.kif 463-469
(=>
    (and
        (instance ?YEAR TimeInterval)
        (holdsDuring ?YEAR
            (economyType ?AREA UpperMiddleIncomeCountry)))
    (and
        (perCapitaGDPInPeriod ?AREA
            (MeasureFn ?AMOUNT UnitedStatesDollar) ?YEAR)
        (greaterThanOrEqualTo ?AMOUNT 2996)))		 Economy.kif 478-484
(=>
    (and
        (instance ?YEAR TimeInterval)
        (holdsDuring ?YEAR
            (economyType ?AREA UpperMiddleIncomeCountry)))
    (and
        (perCapitaGDPInPeriod ?AREA
            (MeasureFn ?AMOUNT UnitedStatesDollar) ?YEAR)
        (lessThan ?AMOUNT 9267)))		 Economy.kif 486-492
(=>
    (and
        (property ?Option Option)
        (optionHolder ?Option ?Agent)
        (strikePrice ?Option ?Price)
        (agreementExpirationDate ?Option ?ExpDate)
        (price ?Stocks ?Price ?Time)
        (instance ?Time TimeInterval)
        (before
            (EndFn ?Time)
            (BeginFn ?ExpDate))
        (underlier ?Option ?Stocks))
    (holdsRight
        (KappaFn ?Sell
            (and
                (instance ?Sell Selling)
                (patient ?Sell ?Stocks)
                (time ?Sell ?Time)
                (measure ?Stocks
                    (MeasureFn 100 ShareUnit))
                (agent ?Sell ?Agent))) ?Agent))		 FinancialOntology.kif 2591-2607
(=>
    (and
        (property ?Option Option)
        (optionHolder ?Option ?Agent)
        (strikePrice ?Option ?Price)
        (agreementExpirationDate ?Option ?ExpDate)
        (underlier ?Option ?Stocks)
        (price ?Stocks ?Price ?Time)
        (instance ?Time TimeInterval)
        (before
            (EndFn ?Time)
            (BeginFn ?ExpDate)))
    (holdsRight
        (KappaFn ?Buy
            (and
                (instance ?Buy Buying)
                (patient ?Buy ?Stocks)
                (time ?Buy ?Time)
                (measure ?Stocks
                    (MeasureFn 100 ShareUnit))
                (agent ?Buy ?Agent))) ?Agent))		 FinancialOntology.kif 2545-2561
(=>
    (and
        (property ?Option Option)
        (optionSeller ?Option ?Agent)
        (strikePrice ?Option ?Price)
        (agreementExpirationDate ?Option ?ExpDate)
        (price ?Stocks ?Price ?Time)
        (instance ?Time TimeInterval)
        (before
            (EndFn ?Time)
            (BeginFn ?ExpDate))
        (underlier ?Option ?Stocks))
    (holdsObligation
        (KappaFn ?Buy
            (and
                (instance ?Buy Buying)
                (patient ?Buy ?Stocks)
                (time ?Buy ?Time)
                (measure ?Stocks
                    (MeasureFn 100 ShareUnit))
                (agent ?Buy ?Agent))) ?Agent))		 FinancialOntology.kif 2609-2625
(=>
    (and
        (property ?Option Option)
        (optionSeller ?Option ?Seller)
        (strikePrice ?Option ?Price)
        (agreementExpirationDate ?Option ?ExpDate)
        (underlier ?Option ?Stocks)
        (price ?Stocks ?Price ?Time)
        (instance ?Time TimeInterval)
        (before
            (EndFn ?Time)
            (BeginFn ?ExpDate)))
    (holdsObligation
        (KappaFn ?Sell
            (and
                (instance ?Sell Selling)
                (patient ?Sell ?Stocks)
                (time ?Sell ?Time)
                (measure ?Stocks
                    (MeasureFn 100 ShareUnit))
                (agent ?Sell ?Agent))) ?Seller))		 FinancialOntology.kif 2563-2581

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent
-------------------------


(<=>
    (overlapsTemporally ?INTERVAL1 ?INTERVAL2)
    (exists (?INTERVAL3)
        (and
            (instance ?INTERVAL3 TimeInterval)
            (temporalPart ?INTERVAL3 ?INTERVAL1)
            (temporalPart ?INTERVAL3 ?INTERVAL2))))		 Merge.kif 7784-7790 时距 时段 和 另一个 时距 重叠 若且唯若 有存在 时间位置 这样 那个 时间位置 是 时距 的 instance 和 那个 时间位置 时段 是 那个 另外 时距 时段 的一 part 和 那个 时间位置 时段 是 那个 时距 时段 的一 part
(=>
    (and
        (holdsDuring ?T1
            (and
                (attribute ?PERSON DislocatedCivilian)
                (inhabits ?PERSON ?RESIDENCE)
                (located ?RESIDENCE ?PLACE)))
        (instance ?PLACE GeographicArea)
        (instance ?T1 TimeInterval))
    (exists (?T0 ?PRIOR-PLACE ?PRIOR-RES)
        (and
            (instance ?T0 TimeInterval)
            (earlier ?T0 ?T1)
            (instance ?PRIOR-RES Object)
            (instance ?PRIOR-PLACE GeopoliticalArea)
            (located ?PRIOR-RES ?PRIOR-PLACE)
            (not
                (equal ?PLACE ?PRIOR-PLACE))
            (not
                (equal ?RESIDENCE ?PRIOR-RES))
            (not
                (geographicSubregion ?PLACE ?PRIOR-PLACE))
            (not
                (geographicSubregion ?PRIOR-PLACE ?PLACE))
            (holdsDuring ?T0
                (inhabits ?PERSON ?PRIOR-RES)))))		 MilitaryPersons.kif 26-47
(=>
    (and
        (instance ?ATC AddToCart)
        (instance ?OBJ Object)
        (patient ?ATC ?OBJ)
        (agent ?ATC ?USER))
    (exists (?COLL ?SITE ?AFTER)
        (and
            (instance ?COLL Collection)
            (instance ?SITE WebSite)
            (instance ?INTERVAL TimeInterval)
            (webcart ?USER ?COLL ?SITE)
            (equal
                (BeginFn ?INTERVAL)
                (EndFn ?ATC))
            (holdsDuring ?AFTER
                (member ?OBJ ?COLL)))))		 UXExperimentalTerms.kif 1522-1538
(=>
    (and
        (instance ?IMPRISON Imprisoning)
        (detainee ?IMPRISON ?AGENT)
        (instance ?AGENT Human)
        (time ?IMPRISON ?INTERVAL)
        (instance ?INTERVAL TimeInterval))
    (exists (?ARREST ?TIME)
        (and
            (instance ?TIME TimeInterval)
            (time ?ARREST ?TIME)
            (earlier ?TIME ?INTERVAL)
            (instance ?ARREST PlacingUnderArrest)
            (arrested ?ARREST ?AGENT))))		 Mid-level-ontology.kif 21468-21481
(=>
    (and
        (instance ?INTERVAL TimeInterval)
        (instance ?SITE WebSite))
    (exists (?NEWBUYERS)
        (and
            (instance ?NEWBUYERS Collection)
            (forall (?AGENT)
                (=>
                    (member ?AGENT ?NEWBUYERS)
                    (and
                        (exists (?BUYING)
                            (and
                                (instance ?AGENT Agent)
                                (instance ?BUYING Buying)
                                (agent ?BUYING ?AGENT)
                                (instrument ?BUYING ?SITE)
                                (during ?BUYING ?INTERVAL)))
                        (not
                            (exists (?INTERVAL_BEFORE)
                                (and
                                    (instance ?INTERVAL_BEFORE TimeInterval)
                                    (earlier ?INTERVAL_BEFORE ?INTERVAL)
                                    (holdsDuring ?INTERVAL_BEFORE
                                        (exists (?BUYING_BEFORE)
                                            (and
                                                (instance ?BUYING_BEFORE Buying)
                                                (agent ?BUYING_BEFORE ?AGENT)
                                                (instrument ?BUYING_BEFORE ?SITE)
                                                (during ?BUYING_BEFORE ?INTERVAL))))))))))
            (equal
                (SiteWideNewBuyersFn ?INTERVAL ?SITE) ?NEWBUYERS))))		 UXExperimentalTerms.kif 3581-3613
(=>
    (and
        (instance ?INTERVAL TimeInterval)
        (instance ?SITE WebSite))
    (exists (?NEWREGISTRATIONS)
        (and
            (instance ?NEWREGISTRATIONS Collection)
            (forall (?USER)
                (=>
                    (and
                        (instance ?USER Human)
                        (not
                            (exists (?INTERVAL_BEFORE)
                                (and
                                    (instance ?INTERVAL_BEFORE TimeInterval)
                                    (earlier ?INTERVAL_BEFORE ?INTERVAL)
                                    (holdsDuring ?INTERVAL_BEFORE
                                        (registeredUser ?USER ?SITE)))))
                        (exists (?INTERVAL_DURING)
                            (and
                                (instance ?INTERVAL_DURING TimeInterval)
                                (during ?INTERVAL_DURING ?INTERVAL)
                                (holdsDuring ?INTERVAL
                                    (registeredUser ?USER ?SITE)))))
                    (member ?USER ?NEWREGISTRATIONS)))
            (equal ?NEWREGISTRATIONS
                (SiteWideNewRegistrationsFn ?INTERVAL ?SITE)))))		 UXExperimentalTerms.kif 3633-3660
(=>
    (and
        (instance ?INTERVAL TimeInterval)
        (instance ?SITE WebSite))
    (exists (?NEWSELLERS)
        (and
            (instance ?NEWSELLERS Collection)
            (forall (?AGENT)
                (=>
                    (member ?AGENT ?NEWSELLERS)
                    (and
                        (exists (?SELLING)
                            (and
                                (instance ?AGENT Agent)
                                (instance ?SELLING Selling)
                                (agent ?SELLING ?AGENT)
                                (instrument ?SELLING ?SITE)
                                (during ?SELLING ?INTERVAL)))
                        (not
                            (exists (?INTERVAL_BEFORE)
                                (and
                                    (instance ?INTERVAL_BEFORE TimeInterval)
                                    (earlier ?INTERVAL_BEFORE ?INTERVAL)
                                    (holdsDuring ?INTERVAL_BEFORE
                                        (exists (?SELLING_BEFORE)
                                            (and
                                                (instance ?SELLING_BEFORE Selling)
                                                (agent ?SELLING_BEFORE ?AGENT)
                                                (instrument ?SELLING_BEFORE ?SITE)
                                                (during ?SELLING_BEFORE ?INTERVAL))))))))))
            (equal
                (SiteWideNewSellersFn ?INTERVAL ?SITE) ?NEWSELLERS))))		 UXExperimentalTerms.kif 3680-3712
(=>
    (and
        (instance ?ORG Organization)
        (attribute ?ORG WarehousingAndStorage))
    (exists (?EV ?MEM)
        (and
            (member ?MEM ?ORG)
            (agent ?MEM ?EV)
            (exists (?P ?OBJ)
                (and
                    (instance ?EV Selling)
                    (instance ?OBJ Object)
                    (instance ?P Human)
                    (patient ?EV ?P)
                    (confersRight
                        (exists (?B ?T)
                            (and
                                (instance ?T TimeInterval)
                                (instance ?B Building)
                                (possesses ?P ?OBJ)
                                (holdsDuring ?T
                                    (located ?B ?OBJ)))) ?MEM ?P))))))		 naics.kif 8699-8720
(=>
    (and
        (instance ?SAW Saw)
        (instance ?CUT Cutting)
        (instrument ?CUT ?SAW)
        (instance ?OBJ Object)
        (patient ?CUT ?OBJ))
    (exists (?MOTION ?DIR1 ?DIR2 ?TIME ?T1 ?T2 ?PART)
        (and
            (instance ?MOTION Motion)
            (subProcess ?MOTION ?CUT)
            (instance ?PART CuttingDevice)
            (part ?PART ?SAW)
            (meetsSpatially ?PART ?OBJ)
            (patient ?MOTION ?PART)
            (instance ?T2 TimeInterval)
            (instance ?T2 TimeInterval)
            (equal
                (WhenFn ?MOTION) ?TIME)
            (temporalPart ?TIME ?T1)
            (temporalPart ?TIME ?T2)
            (instance ?DIR1 DirectionalAttribute)
            (instance ?DIR2 DirectionalAttribute)
            (=>
                (holdsDuring ?T1
                    (direction ?MOTION ?DIR1))
                (holdsDuring ?T2
                    (and
                        (direction ?MOTION ?DIR2)
                        (or
                            (equal ?DIR1 ?DIR2)
                            (oppositeDirection ?DIR1 ?DIR2))
                        (not
                            (and
                                (equal ?DIR1 ?DIR2)
                                (oppositeDirection ?DIR1 ?DIR2)))))))))		 Mid-level-ontology.kif 15871-15905
(=>
    (and
        (instance ?WATCH WatchItem)
        (instance ?OBJ Object)
        (patient ?WATCH ?OBJ)
        (agent ?WATCH ?USER))
    (exists (?COLL ?SITE ?AFTER)
        (and
            (instance ?COLL Collection)
            (instance ?SITE WebSite)
            (instance ?INTERVAL TimeInterval)
            (watchingListings ?USER ?COLL ?SITE)
            (equal
                (BeginFn ?INTERVAL)
                (EndFn ?WATCH))
            (holdsDuring ?AFTER
                (member ?OBJ ?COLL)))))		 UXExperimentalTerms.kif 1811-1827
(=>
    (and
        (newRegisteredUsers ?INT ?SITE ?COLL)
        (member ?MEMBER ?COLL))
    (exists (?DURING)
        (and
            (instance ?DURING TimeInterval)
            (during ?DURING ?INT)
            (holdsDuring ?DURING
                (registeredUser ?MEMBER ?SITE)))))		 UXExperimentalTerms.kif 3834-3843
(=>
    (and
        (newRegisteredUsers ?INT1 ?SITE ?COLL)
        (member ?MEMBER ?COLL))
    (not
        (exists (?INT2)
            (and
                (instance ?INT2 TimeInterval)
                (earlier ?INT2 ?INT1)
                (holdsDuring ?INT2
                    (registeredUser ?MEMBER ?SITE))))))		 UXExperimentalTerms.kif 3845-3855
(=>
    (and
        (property ?Option EuropeanStyleOption)
        (agreementExpirationDate ?Option ?Date))
    (exists (?Period ?Time)
        (and
            (instance ?Period TimeInterval)
            (finishes ?Period ?Date)
            (=>
                (and
                    (instance ?Exercise ExerciseAnOption)
                    (equal
                        (WhenFn ?Exercise) ?Time))
                (temporalPart ?Time ?Period)))))		 FinancialOntology.kif 2729-2741
(=>
    (and
        (rentalPrice ?OBJ ?QUANT ?AGENT ?PS)
        (equal ?QUANT
            (PerFn ?PRICE ?TIME))
        (immediateInstance ?ITEM ?OBJ)
        (instance ?R Renting)
        (patient ?R ?ITEM)
        (possesses ?OBJ ?AGENT)
        (agent ?R ?CUSTOMER)
        (time ?R ?TIMEINT))
    (forall (?X)
        (=>
            (and
                (during ?TIMEINT ?X)
                (instance ?X TimeInterval)
                (duration ?X ?DURATION)
                (lessThanOrEqualTo ?DURATION ?TIME))
            (exists (?P)
                (and
                    (instance ?P Payment)
                    (destination ?P ?AGENT)
                    (agent ?P ?CUSTOMER)
                    (transactionAmount ?P ?PRICE))))))		 Catalog.kif 450-472
(=>
    (holdsDuring ?T1
        (inhabits ?ORGANISM ?OBJ))
    (exists (?TIME)
        (and
            (instance ?TIME TimeInterval)
            (temporalPart ?TIME ?T1)
            (holdsDuring ?TIME
                (located ?ORGANISM ?OBJ)))))		 Merge.kif 13361-13367
(=>
    (instance ?C Convoy)
    (exists (?V1 ?V2 ?TIME)
        (and
            (not
                (equal ?V1 ?V2))
            (instance ?V1 Vehicle)
            (instance ?V2 Vehicle)
            (instance ?TIME TimeInterval)
            (temporalPart ?TIME
                (WhenFn ?C))
            (holdsDuring ?TIME
                (and
                    (member ?V1 ?C)
                    (member ?V2 ?C))))))		 Mid-level-ontology.kif 20212-20224
(=>
    (instance ?D Disappearing)
    (exists (?OBJ ?AGENT ?SEARCH ?TIME)
        (and
            (instance ?SEARCH Searching)
            (earlier
                (WhenFn ?D)
                (WhenFn ?SEARCH))
            (agent ?SEARCH ?AGENT)
            (instance ?OBJ Object)
            (patient ?D ?OBJ)
            (patient ?SEARCH ?OBJ)
            (instance ?TIME TimeInterval)
            (temporalPart ?TIME
                (WhenFn ?SEARCH))
            (holdsDuring ?TIME
                (not
                    (modalAttribute
                        (exists (?DISC)
                            (and
                                (instance ?DISC Discovering)
                                (agent ?DISC ?AGENT)
                                (patient ?DISC ?OBJ))) Possibility))))))		 Mid-level-ontology.kif 14911-14933
(=>
    (instance ?LIST ListOnSite)
    (exists (?SITE ?ADVERT ?EARLIER ?AFTER)
        (and
            (instance ?SITE WebSite)
            (instance ?ADVERT WebListing)
            (instance ?EARLIER TimeInterval)
            (instance ?AFTER TimeInterval)
            (patient ?LIST ?ADVERT)
            (equal
                (EndFn ?EARLIER)
                (EndFn ?LIST))
            (earlier ?LIST ?AFTER)
            (meetsTemporally ?LIST ?AFTER)
            (holdsDuring ?EARLIER
                (not
                    (hostedOn ?ADVERT ?SITE)))
            (holdsDuring ?AFTER
                (hostedOn ?ADVERT ?SITE))
            (agent ?LIST ?OWNER)
            (possesses ?OWNER ?SITE))))		 UXExperimentalTerms.kif 338-358
(=>
    (instance ?POINT TimePoint)
    (exists (?INTERVAL)
        (and
            (instance ?INTERVAL TimeInterval)
            (temporalPart ?POINT ?INTERVAL))))		 Merge.kif 7545-7550

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 1972-1980 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体


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