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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - time
time

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


(documentation time ChineseLanguage "这个关系用于一个 Physical 实例 和一个 TimePosition 实例之间,以防前者所存在的的时间包含了后者的。 换句话说,(time ?THING ?TIME) 的意思是 ?THING 在 ?TIME 出现或发生。注: time 在于 Physical 实例,就相等于 holdsDuring 用在 Formula 的实例上,常数 locatedtime 分别是是基本的空间和时间谓词。") chinese_format.kif 2079-2082
(documentation time EnglishLanguage "This relation holds between an instance of Physical and an instance of TimePosition just in case the temporal lifespan of the former includes the latter. In other words, (time ?THING ?TIME) means that ?THING existed or occurred at ?TIME. Note that time does for instances of time what holdsDuring does for instances of Formula. The constants located and time are the basic spatial and temporal predicates, respectively.") Merge.kif 3740-3746
(domain time 1 Physical) Merge.kif 3735-3735 The number 1 argument of time is an instance of physical
(domain time 2 TimePosition) Merge.kif 3736-3736 The number 2 argument of time is an instance of time position
(instance time AsymmetricRelation) Merge.kif 3733-3733 time is an instance of asymmetric relation
(instance time BinaryPredicate) Merge.kif 3731-3731 time is an instance of binary predicate
(instance time TemporalRelation) Merge.kif 3732-3732 time is an instance of temporal relation
(instance time TotalValuedRelation) Merge.kif 3734-3734 time is an instance of total valued relation
(relatedInternalConcept time holdsDuring) Merge.kif 3738-3738 time is internally related to holds during
(relatedInternalConcept time located) Merge.kif 3737-3737 time is internally related to located

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


(format ChineseLanguage time "%1 在 %2 是 %n{doesn't} 存在") chinese_format.kif 191-191
(format EnglishLanguage time "%1 %n{doesn't} exist%p{s} during %2") english_format.kif 195-195
(subrelation date time) Merge.kif 8035-8035 date is a subrelation of time
(termFormat ChineseLanguage time "时间") chinese_format.kif 192-192
(termFormat ChineseTraditionalLanguage time "時間") domainEnglishFormat.kif 58083-58083
(termFormat EnglishLanguage time "time") domainEnglishFormat.kif 58082-58082

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


(<=>
    (and
        (time ?PHYS ?TIME)
        (instance ?TIME TimePoint))
    (temporallyBetweenOrEqual
        (BeginFn
            (WhenFn ?PHYS)) ?TIME
        (EndFn
            (WhenFn ?PHYS))))
Merge.kif 7782-7786 A physical exists during a time point and the time point is an instance of time point if and only if the time point is between or at the beginning of the time of existence of the physical and the end of the time of existence of the physical
(=>
    (and
        (instance ?Exercise ExerciseAnOption)
        (patient ?Exercise ?Option)
        (property ?Option CallOption)
        (time ?Exercise ?Time)
        (underlier ?Option ?Stocks))
    (exists (?Buy)
        (and
            (instance ?Buy Buying)
            (patient ?Buy ?Stocks)
            (time ?Buy ?Time)
            (measure ?Stocks
                (MeasureFn 100 ShareUnit)))))
FinancialOntology.kif 2694-2706
(=>
    (and
        (instance ?Exercise ExerciseAnOption)
        (patient ?Exercise ?Option)
        (property ?Option PutOption)
        (time ?Exercise ?Time)
        (underlier ?Option ?Stocks))
    (exists (?Sell)
        (and
            (instance ?Sell Selling)
            (patient ?Sell ?Stocks)
            (time ?Sell ?Time)
            (measure ?Stocks
                (MeasureFn 100 ShareUnit)))))
FinancialOntology.kif 2708-2720
(=>
    (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 19950-19963
(=>
    (and
        (instance ?Refinancing Refinancing)
        (time ?Refinancing ?Time)
        (instance ?Loan Loan)
        (securedBy ?Loan ?Collateral)
        (borrower ?Loan ?Borrower)
        (currentAccountBalance ?Loan ?Time ?Amount)
        (patient ?Refinancing ?Loan))
    (exists (?NewLoan ?Payment)
        (and
            (instance ?NewLoan Loan)
            (borrower ?NewLoan ?Borrower)
            (securedBy ?Loan ?Collateral)
            (destination ?Payment
                (CurrencyFn ?Loan))
            (time ?Payment ?Time)
            (origin ?Payment
                (CurrencyFn ?NewLoan))
            (transactionAmount ?Payment ?Amount))))
FinancialOntology.kif 1403-1420
(=>
    (and
        (instance ?SEEING Seeing)
        (patient ?SEEING ?OBJ)
        (agent ?SEEING ?AGENT)
        (instance ?OBJ Object)
        (time ?SEEING ?TIME)
        (holdsDuring ?TIME
            (located ?OBJ ?PLACE)))
    (observedAtTimeInPlace ?OBJ ?AGENT ?TIME ?PLACE))
Justice.kif 61-69
(=>
    (and
        (playsRoleInEvent ?OBJ ?ROLE ?EVENT)
        (instance ?EVENT ?CLASS)
        (subclass ?CLASS Process)
        (time ?EVENT ?TIME)
        (eventLocated ?EVENT ?PLACE))
    (playsRoleInEventOfType ?OBJ ?ROLE ?CLASS ?TIME ?PLACE))
Mid-level-ontology.kif 19697-19704
(=>
    (and
        (playsRoleInEvent ?OBJ ?ROLE ?EVENT)
        (instance ?EVENT ?TYPE)
        (subclass ?TYPE Process)
        (time ?EVENT ?TIME)
        (eventLocated ?EVENT ?PLACE))
    (playsRoleInEventOfType ?OBJ ?ROLE ?TYPE ?TIME ?PLACE))
Mid-level-ontology.kif 19726-19733
(=>
    (and
        (playsRoleInEvent ?OBJ ?ROLE ?EVENT)
        (time ?EVENT ?TIME)
        (eventLocated ?EVENT ?PLACE))
    (locatedAtTime ?OBJ ?TIME ?PLACE))
Mid-level-ontology.kif 19749-19754
(=>
    (and
        (rentalPrice ?OBJ ?QUANT ?AGENT ?PS)
        (equal ?QUANT
            (PerFn ?PRICE
                (measure ?TIME ?U)))
        (instance ?U UnitOfDuration)
        (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
                    (MeasureFn ?DURATION ?U))
                (lessThanOrEqualTo ?DURATION ?TIME))
            (exists (?P)
                (and
                    (instance ?P Payment)
                    (destination ?P ?AGENT)
                    (agent ?P ?CUSTOMER)
                    (transactionAmount ?P ?PRICE))))))
Catalog.kif 458-483
(=>
    (and
        (taxDeferredIncome ?Agent ?Income ?Activity)
        (time ?Activity ?Time))
    (not
        (exists (?Tax)
            (and
                (instance ?Tax Tax)
                (causes ?Activity ?Tax)
                (time ?Tax ?Time)))))
FinancialOntology.kif 3252-3261

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


(<=>
    (instance ?PROCESS Creation)
    (exists (?PATIENT)
        (and
            (patient ?PROCESS ?PATIENT)
            (time ?PATIENT
                (EndFn
                    (WhenFn ?PROCESS)))
            (not
                (time ?PATIENT
                    (BeginFn
                        (WhenFn ?PROCESS)))))))
Merge.kif 11902-11909 A process is an instance of creation if and only if there exists a physical such that the physical is a patient of the process and the physical exists during the end of the time of existence of the process and the physical doesn't exist during the beginning of the time of existence of the process
(<=>
    (instance ?PROCESS Destruction)
    (exists (?PATIENT)
        (and
            (patient ?PROCESS ?PATIENT)
            (time ?PATIENT
                (BeginFn
                    (WhenFn ?PROCESS)))
            (not
                (time ?PATIENT
                    (EndFn
                        (WhenFn ?PROCESS)))))))
Merge.kif 11450-11457 A process is an instance of destruction if and only if there exists a physical such that the physical is a patient of the process and the physical exists during the beginning of the time of existence of the process and the physical doesn't exist during the end of the time of existence of the process
(<=>
    (temporalPart ?POS
        (WhenFn ?THING))
    (time ?THING ?POS))
Merge.kif 7589-7591 A time position is a part of the time of existence of a physical if and only if the physical exists during the time position
(=>
    (agreementAdoptionDate ?AGR ?DATE)
    (exists (?PROCESS ?DAY)
        (and
            (instance ?PROCESS Committing)
            (instance ?DAY ?DATE)
            (patient ?PROCESS ?AGR)
            (time ?PROCESS ?DAY))))
Government.kif 693-700
(=>
    (and
        (holdsDuring ?INTERVAL
            (?REL ?INST1 ?INST2))
        (instance ?INST1 Physical)
        (instance ?INST2 Physical))
    (and
        (time ?INST1 ?INTERVAL)
        (time ?INST2 ?INTERVAL)))
Merge.kif 7580-7587
(=>
    (and
        (instance ?CLOSE ClosingGraphicalWindow)
        (patient ?CLOSE ?WINDOW))
    (and
        (instance ?WINDOW InterfaceWindow)
        (time ?WINDOW
            (BeginFn
                (WhenFn ?OPEN)))
        (not
            (time ?WINDOW
                (EndFn
                    (WhenFn ?OPEN))))))
ComputerInput.kif 2453-2460
(=>
    (and
        (instance ?Check Check)
        (instance ?Processing ProcessingACheck)
        (patient ?Processing ?Check))
    (exists (?Depositing)
        (and
            (instance ?Depositing DepositingACheck)
            (patient ?Depositing ?Check)
            (time ?Depositing
                (ImmediatePastFn
                    (WhenFn ?Processing))))))
FinancialOntology.kif 137-146
(=>
    (and
        (instance ?Exercise ExerciseAnOption)
        (patient ?Exercise ?Option)
        (property ?Option CallOption)
        (time ?Exercise ?Time)
        (underlier ?Option ?Stocks))
    (exists (?Buy)
        (and
            (instance ?Buy Buying)
            (patient ?Buy ?Stocks)
            (time ?Buy ?Time)
            (measure ?Stocks
                (MeasureFn 100 ShareUnit)))))
FinancialOntology.kif 2694-2706
(=>
    (and
        (instance ?Exercise ExerciseAnOption)
        (patient ?Exercise ?Option)
        (property ?Option PutOption)
        (time ?Exercise ?Time)
        (underlier ?Option ?Stocks))
    (exists (?Sell)
        (and
            (instance ?Sell Selling)
            (patient ?Sell ?Stocks)
            (time ?Sell ?Time)
            (measure ?Stocks
                (MeasureFn 100 ShareUnit)))))
FinancialOntology.kif 2708-2720
(=>
    (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 19950-19963
(=>
    (and
        (instance ?Loan CallableLoan)
        (lender ?Loan ?Lender)
        (borrower ?Loan ?Borrower)
        (totalBalance ?Loan ?Amount)
        (instance ?Call Call)
        (agent ?Call ?Lender)
        (patient ?Call ?Loan))
    (holdsObligation
        (KappaFn ?Payment
            (and
                (destination ?Payment ?Lender)
                (time ?Payment
                    (ImmediateFutureFn
                        (WhenFn ?Call)))
                (transactionAmount ?Payment ?Amount))) ?Borrower))
FinancialOntology.kif 1382-1397
(=>
    (and
        (instance ?O OccupationalRole)
        (typicalAction ?PCLASS
            (AttrFn CognitiveAgent ?O)))
    (exists (?X ?T ?P ?PT)
        (and
            (instance ?X CognitiveAgent)
            (holdsDuring ?T
                (attribute ?X ?O))
            (instance ?P ?PCLASS)
            (agent ?X ?P)
            (time ?P ?PT)
            (temporalPart ?PT ?T))))
Mid-level-ontology.kif 18730-18743
(=>
    (and
        (instance ?Refinancing Refinancing)
        (time ?Refinancing ?Time)
        (instance ?Loan Loan)
        (securedBy ?Loan ?Collateral)
        (borrower ?Loan ?Borrower)
        (currentAccountBalance ?Loan ?Time ?Amount)
        (patient ?Refinancing ?Loan))
    (exists (?NewLoan ?Payment)
        (and
            (instance ?NewLoan Loan)
            (borrower ?NewLoan ?Borrower)
            (securedBy ?Loan ?Collateral)
            (destination ?Payment
                (CurrencyFn ?Loan))
            (time ?Payment ?Time)
            (origin ?Payment
                (CurrencyFn ?NewLoan))
            (transactionAmount ?Payment ?Amount))))
FinancialOntology.kif 1403-1420
(=>
    (and
        (monitorComponentData ?Time1 ?ID ?Number)
        (componentDataID ?Time2 ?Component ?Instance ?Unit ?ID))
    (exists (?Event)
        (and
            (instance ?Event MeasuringPerformance)
            (unitMeasuringPerformance ?Instance ?Unit)
            (time ?Event ?Time1)
            (performanceResult ?Event ?Instance ?Number))))
QoSontology.kif 953-962
(=>
    (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 2610-2626
(=>
    (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 2564-2580
(=>
    (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 2628-2644
(=>
    (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 2582-2600
(=>
    (and
        (taxDeferredIncome ?Agent ?Income ?Activity)
        (time ?Activity ?Time))
    (not
        (exists (?Tax)
            (and
                (instance ?Tax Tax)
                (causes ?Activity ?Tax)
                (time ?Tax ?Time)))))
FinancialOntology.kif 3252-3261
(=>
    (baptismdate ?PERSON ?DAY)
    (exists (?BAPTISM)
        (and
            (instance ?BAPTISM Baptizing)
            (experiencer ?BAPTISM ?PERSON)
            (time ?BAPTISM ?DAY))))
Biography.kif 68-74
(=>
    (instance ?OBJ Object)
    (exists (?TIME1 ?TIME2)
        (and
            (instance ?TIME1 TimePoint)
            (instance ?TIME2 TimePoint)
            (before ?TIME1 ?TIME2)
            (forall (?TIME)
                (=>
                    (and
                        (beforeOrEqual ?TIME1 ?TIME)
                        (beforeOrEqual ?TIME ?TIME2))
                    (time ?OBJ ?TIME))))))
Merge.kif 7704-7716
(=>
    (instance ?OPEN OpeningNewGraphicalWindow)
    (exists (?WINDOW)
        (and
            (patient ?OPEN ?WINDOW)
            (instance ?WINDOW InterfaceWindow)
            (time ?WINDOW
                (EndFn
                    (WhenFn ?OPEN)))
            (not
                (time ?WINDOW
                    (BeginFn
                        (WhenFn ?OPEN)))))))
ComputerInput.kif 2388-2395
(=>
    (instance ?PHYS Physical)
    (exists (?LOC ?TIME)
        (and
            (located ?PHYS ?LOC)
            (time ?PHYS ?TIME))))
Merge.kif 804-809
(=>
    (instance ?Spread SpreadOption)
    (exists (?Option1 ?Option2 ?Buy ?Sell ?Time)
        (and
            (instance ?Option1 Option)
            (instance ?Option2 Option)
            (instance ?Buy Buying)
            (instance ?Sell Selling)
            (subProcess ?Buy ?Spread)
            (subProcess ?Sell ?Spread)
            (patient ?Buy ?Option1)
            (patient ?Sell ?Option2)
            (time ?Buy ?Time)
            (time ?Sell ?Time))))
FinancialOntology.kif 3037-3050
(=>
    (monitorApplicationData ?Time ?Application)
    (exists (?Process)
        (and
            (programRunning ?Process ?Application)
            (time ?Process ?Time))))
QoSontology.kif 977-982

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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