TreeView Knowledge Base Browser

appearance as argument number 1

s__documentation(s__EndFn__m,s__ChineseLanguage,'"这是一个 UnaryFunction，它把一个 TimeInterval 和这个时段结束的 TimePoint联系起来。"')	chinese_format.kif 2699-2700
s__documentation(s__EndFn__m,s__EnglishLanguage,'"A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval ends."')	Merge.kif 7779-7780
s__domain(s__EndFn__m,n__1,s__TimeInterval)	Merge.kif 7776-7776	The number 1 argument of end is an instance of time interval
s__instance(s__EndFn__m,s__TemporalRelation) s__instance(s__TemporalRelation,s__Class)	Merge.kif 7773-7773	End is an instance of temporal relation
s__instance(s__TotalValuedRelation,s__Class) s__instance(s__EndFn__m,s__TotalValuedRelation)	Merge.kif 7775-7775	End is an instance of total valued relation
s__instance(s__UnaryFunction,s__Class) s__instance(s__EndFn__m,s__UnaryFunction)	Merge.kif 7774-7774	End is an instance of unary function
s__range(s__EndFn__m,s__TimePoint)	Merge.kif 7777-7777	The range of end is an instance of time point

appearance as argument number 2

s__format(s__ChineseLanguage,s__EndFn__m,'"%1 的结束"')	chinese_format.kif 451-451
s__format(s__EnglishLanguage,s__EndFn__m,'"the end of %1"')	english_format.kif 460-460
s__termFormat(s__ChineseLanguage,s__EndFn__m,'"结束"')	domainEnglishFormat.kif 22035-22035
s__termFormat(s__ChineseLanguage,s__EndFn__m,'"结束函数"')	chinese_format.kif 452-452
s__termFormat(s__ChineseTraditionalLanguage,s__EndFn__m,'"結束"')	domainEnglishFormat.kif 22034-22034
s__termFormat(s__EnglishLanguage,s__EndFn__m,'"end"')	domainEnglishFormat.kif 22033-22033

antecedent

( ! [V__AGENT,V__PROCESS,V__PROCESSSTART,V__AGENTEND] : (((s__instance(V__AGENT,s__Agent) & s__instance(V__PROCESS,s__Process) & s__instance(V__PROCESSSTART,s__TimePoint) & s__instance(V__AGENTEND,s__TimePoint)) => ((((V__PROCESSSTART = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENTEND = s__EndFn(s__WhenFn(V__AGENT))) & s__benefits(V__PROCESS,V__AGENT)) => (s__before(V__PROCESSSTART,V__AGENTEND))))) ) )	Mid-level-ontology.kif 22011-22016	If a time point is equal to the beginning of the time of existence of a process and another time point is equal to the end of the time of existence of an agent and the agent is a beneficiary of the process, then the time point happens before the other time point
( ! [V__AGENT,V__PROCESS,V__PROCESSSTART,V__AGENTEND] : (((s__instance(V__AGENT,s__Agent) & s__instance(V__PROCESS,s__Process) & s__instance(V__PROCESSSTART,s__TimePoint) & s__instance(V__AGENTEND,s__TimePoint)) => ((((V__PROCESSSTART = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENTEND = s__EndFn(s__WhenFn(V__AGENT))) & s__suffers(V__PROCESS,V__AGENT)) => (s__before(V__PROCESSSTART,V__AGENTEND))))) ) )	Mid-level-ontology.kif 28654-28663	If a time point is equal to the beginning of the time of existence of a process and another time point is equal to the end of the time of existence of an agent and the agent suffers from the process, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11794-11808	If a process is an instance of attaching and an entity is a patient of the process and another entity is a patient of the process and the entity is not connected to the other entity holds during the beginning of the time of existence of the process and the entity is connected to the other entity holds during the end of the time of existence of the process, then the process attaches the entity to another object and the process attaches the other entity to another object
( ! [V__PAGE,V__ACCESSING,V__INTERVAL,V__REQUESTING,V__BROWSER,V__TRANSFER,V__SERVER] : (((s__instance(V__ACCESSING,s__AccessingWebPage) & s__instance(V__PAGE,s__WebPage) & s__instance(V__TRANSFER,s__DataTransfer) & s__instance(V__SERVER,s__Server) & s__instance(V__REQUESTING,s__Requesting) & s__instance(V__BROWSER,s__WebBrowser) & s__instance(V__INTERVAL,s__TimeInterval) & s__patient(V__ACCESSING,V__PAGE) & s__agent(V__REQUESTING,V__BROWSER) & s__destination(V__REQUESTING,V__SERVER) & s__patient(V__REQUESTING,V__PAGE) & s__origin(V__TRANSFER,V__SERVER) & s__destination(V__TRANSFER,V__BROWSER) & s__patient(V__TRANSFER,V__PAGE) & s__subProcess(V__TRANSFER,V__ACCESSING) & s__subProcess(V__REQUESTING,V__ACCESSING) & (s__EndFn(s__WhenFn(V__REQUESTING)) = s__BeginFn(V__INTERVAL)) & (s__EndFn(s__WhenFn(V__TRANSFER)) = s__EndFn(V__INTERVAL))) => ((s__SiteSpeedFn(V__ACCESSING) = V__INTERVAL))) ) )	UXExperimentalTerms.kif 3966-3991	If an AccessingWebPage is an instance of AccessingWebPage and an entity is an instance of WebPage and a process is an instance of data transfer and an object is an instance of server and another process is an instance of requesting and an agent is an instance of web browser and a time interval is an instance of time interval and the entity is a patient of the AccessingWebPage and the agent is an agent of the other process and the other process ends up at the object and the entity is a patient of the other process and the process originates at the object and the process ends up at the agent and the entity is a patient of the process and the process is a subprocess of the AccessingWebPage and the other process is a subprocess of the AccessingWebPage and the end of the time of existence of the other process is equal to the beginning of the time interval and the end of the time of existence of the process is equal to the end of the time interval, then the time to access in the AccessingWebPage is equal to the time interval
( ! [V__CD,V__DateOfWithdrawal,V__Withdrawal,V__MaturityDate] : (((s__instance(V__DateOfWithdrawal,s__Day) & s__instance(V__MaturityDate,s__Day)) => (((s__instance(V__CD,s__CertificateOfDeposit) & s__maturityDate(V__CD,V__MaturityDate) & s__instance(V__Withdrawal,s__Withdrawal) & s__origin(V__Withdrawal,s__CurrencyFn(V__CD)) & s__date(V__Withdrawal,V__DateOfWithdrawal) & s__before(s__EndFn(V__DateOfWithdrawal) ,s__BeginFn(V__MaturityDate))) => (( ? [V__Penalty] : ((s__instance(V__Penalty,s__Penalty) & s__destination(V__Penalty,s__CurrencyFn(V__CD)) & s__causes(V__Withdrawal,V__Penalty)))))))) ) )	FinancialOntology.kif 1041-1053	If a financial account is an instance of certificate of deposit and a day is a maturity date of the financial account and a process is an instance of withdrawal and the process originates at the currency of the financial account and date of the process is another day and the end of the other day happens before the beginning of the day, then there exists another process such that the other process is an instance of penalty and the other process ends up at the currency of the financial account and the process causes the other process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11153-11160	If a process is an instance of change of possession and an entity is a patient of the process and another entity possesses the entity holds during the beginning of the time of existence of the process and a third entity possesses the entity holds during the end of the time of existence of the process, then the other entity is not equal to the third entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11842-11851	If a process is an instance of detaching and an entity is a patient of the process and another entity is a patient of the process and the entity is connected to the other entity holds during the beginning of the time of existence of the process and the entity is not connected to the other entity holds during the end of the time of existence of another process, then the other process detaches the entity from another object and the other process detaches the other entity from another object
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2459-2469	If a process is an instance of exporting and an entity is a patient of the process and an object is an instance of geopolitical area and a physical is an instance of geopolitical area and the entity is located at the object holds during the beginning of the time of existence of the process and the entity is located at the physical holds during the end of the time of existence of the process, then the physical is not located at the object
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL1,s__TimeInterval) & s__instance(V__INTERVAL2,s__TimeInterval) & (s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & (s__EndFn(V__INTERVAL1) = s__EndFn(V__INTERVAL2))) => ((V__INTERVAL1 = V__INTERVAL2))) ) )	Merge.kif 8004-8014	If a time interval is an instance of time interval and another time interval is an instance of time interval and the beginning of the time interval is equal to the beginning of the other time interval and the end of the time interval is equal to the end of the other time interval, then the time interval is equal to the other time interval
( ! [V__AGENT,V__PROCESS,V__ACCESSING,V__TIMETOFIRST,V__PROCESS_CLASS] : (((s__instance(V__PROCESS,s__TimeInterval) & s__instance(V__PROCESS,s__Process) & s__instance(V__PROCESS_CLASS,s__Class)) => (((s__instance(V__PROCESS,V__PROCESS_CLASS) & s__subclass(V__PROCESS_CLASS,s__Process) & s__instance(V__ACCESSING,s__AccessingWebPage) & s__instance(V__AGENT,s__Agent) & s__agent(V__PROCESS,V__AGENT) & s__agent(V__ACCESSING,V__AGENT) & s__during(V__PROCESS,V__ACCESSING) & s__instance(V__TIMETOFIRST,s__TimeInterval) & ~(( ? [V__PROCESS2] : ((s__instance(V__PROCESS2,s__TimeInterval) & s__instance(V__PROCESS2,s__Process) & (s__instance(V__PROCESS2,V__PROCESS_CLASS) & s__agent(V__PROCESS2,V__AGENT) & s__during(V__PROCESS2,V__ACCESSING) & s__before(s__BeginFn(s__WhenFn(V__PROCESS2)) ,s__BeginFn(s__WhenFn(V__PROCESS)))))))) & (s__BeginFn(s__WhenFn(V__ACCESSING)) = s__BeginFn(s__WhenFn(V__TIMETOFIRST))) & (s__BeginFn(s__WhenFn(V__PROCESS)) = s__EndFn(s__WhenFn(V__TIMETOFIRST)))) => ((s__TTFxFn(V__PROCESS_CLASS,V__ACCESSING) = V__TIMETOFIRST))))) ) )	UXExperimentalTerms.kif 1703-1725	If a time interval is an instance of the time interval_CLASS and the time interval_CLASS is a subclass of process and an AccessingWebPage is an instance of AccessingWebPage and an agent is an instance of agent and the agent is an agent of the time interval and the agent is an agent of the AccessingWebPage and the time interval takes place during the AccessingWebPage and a physical is an instance of time interval and there doesn't exist the time interval2 such that the time interval2 is an instance of the time interval_CLASS and the agent is an agent of the time interval2 and the time interval2 takes place during the AccessingWebPage and the beginning of the time of existence of the time interval2 happens before the beginning of the time of existence of the time interval and the beginning of the time of existence of the AccessingWebPage is equal to the beginning of the time of existence of the physical and the beginning of the time of existence of the time interval is equal to the end of the time of existence of the physical, then the time of the AccessingWebPage in the class the time interval_CLASS is equal to the physical
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2631-2647	If an agreement the attribute option and a cognitive agent holds the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval and the financial instrument is an underlier of the agreement, then the cognitive agent has the right to perform the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2585-2601	If an agreement the attribute option and a cognitive agent holds the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is an underlier of the agreement and the financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval, then the cognitive agent has the right to perform the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2649-2665	If an agreement the attribute option and a cognitive agent sells the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval and the financial instrument is an underlier of the agreement, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2603-2621	If an agreement the attribute option and a cognitive agent sells the agreement and a currency measure is a strike price of the agreement and the agreement has expiration a time interval and a financial instrument is an underlier of the agreement and the financial instrument is price the currency measure for an agent and the agent is an instance of time interval and the end of the agent happens before the beginning of the time interval, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7791-7796	If an object is a resource for a process and the measure of the object is a quantity holds during the beginning of the time of existence of the process and the measure of the object is another quantity holds during the end of the time of existence of the process, then the quantity is greater than the other quantity
( ! [V__Amount,V__Date,V__Account,V__Payment,V__DueDate] : (((s__instance(V__Amount,s__CurrencyMeasure) & s__instance(V__Date,s__Day) & s__instance(V__Payment,s__FinancialTransaction) & s__instance(V__DueDate,s__TimeInterval)) => (((s__transactionAmount(V__Payment,V__Amount) & s__date(V__Payment,V__Date) & s__instance(V__Account,s__FinancialAccount) & s__destination(V__Payment,s__CurrencyFn(V__Account)) & s__amountDue(V__Account,V__Amount,V__DueDate) & s__before(s__EndFn(V__Date) ,s__BeginFn(V__DueDate))) => (s__instance(V__Payment,s__Prepayment))))) ) )	FinancialOntology.kif 788-796	If a currency measure is a transaction amount of a financial transaction and date of the financial transaction is a day and a financial account is an instance of financial account and the financial transaction ends up at the currency of the financial account and the financial account amount due the currency measure for a time interval and the end of the day happens before the beginning of the time interval, then the financial transaction is an instance of prepayment
( ! [V__INTERVAL,V__POINT] : (((s__instance(V__INTERVAL,s__TimeInterval) & s__instance(V__POINT,s__TimePoint)) => (((s__EndFn(V__INTERVAL) = V__POINT) => (( ! [V__OTHERPOINT] : ((s__instance(V__OTHERPOINT,s__TimePoint) => (((s__temporalPart(V__OTHERPOINT,V__INTERVAL) & ~((V__OTHERPOINT = V__POINT))) => (s__before(V__OTHERPOINT,V__POINT))))))))))) ) )	Merge.kif 7782-7789	If the end of a time interval is equal to a time point, then for all another time point if the other time point is a part of the time interval and the other time point is not equal to the time point, then the other time point happens before the time point
( ! [V__Time,V__Process1,V__Program1,V__Process2,V__Delay,V__Program2] : (((s__instance(V__Time,s__TimeInterval) & s__instance(V__Program1,s__ComputerProgram) & s__instance(V__Delay,s__TimeDuration) & s__instance(V__Program2,s__ComputerProgram)) => ((( ? [V__Time1, V__Time2] : ((s__instance(V__Time1,s__TimeInterval) & s__instance(V__Time2,s__TimeInterval) & (s__dependencyDelay(V__Program1,V__Delay) & s__dependencyType(V__Program1,s__ShutdownBlock) & s__hasDependency(V__Program1,V__Program2) & s__instance(V__Process1,s__ComputerProcess) & s__programRunning(V__Process1,V__Program1) & s__instance(V__Process2,s__ComputerProcess) & s__programRunning(V__Process2,V__Program2) & (s__WhenFn(V__Process2) = V__Time2) & s__finishes(V__Time,V__Time1) & (s__WhenFn(V__Process2) = V__Time2) & (s__BeginFn(V__Time) = s__EndFn(V__Time2)))))) => (s__duration(V__Time,V__Delay))))) ) )	QoSontology.kif 1275-1289	If there exist a time interval and another time interval such that a time duration is a dependency delay of a computer program and shutdown block is a dependency type of the computer program and another computer program has a dependency on the computer program and a computer process is an instance of computer process and the computer program is a program running of the computer process and another computer process is an instance of computer process and the other computer program is a program running of the other computer process and the time of existence of the other computer process is equal to the other time interval and a third time interval finishes the time interval and the time of existence of the other computer process is equal to the other time interval and the beginning of the third time interval is equal to the end of the other time interval, then duration of the third time interval is the time duration
( ! [V__Time,V__Process1,V__Program1,V__Process2,V__Delay,V__Program2] : (((s__instance(V__Time,s__TimeInterval) & s__instance(V__Program1,s__ComputerProgram) & s__instance(V__Delay,s__TimeDuration) & s__instance(V__Program2,s__ComputerProgram)) => ((( ? [V__Time1, V__Time2] : ((s__instance(V__Time1,s__TimeInterval) & s__instance(V__Time2,s__TimeInterval) & (s__dependencyDelay(V__Program1,V__Delay) & s__dependencyType(V__Program1,s__StartupBlock) & s__hasDependency(V__Program1,V__Program2) & s__instance(V__Process1,s__ComputerProcess) & s__programRunning(V__Process1,V__Program1) & s__instance(V__Process2,s__ComputerProcess) & s__programRunning(V__Process2,V__Program2) & (s__WhenFn(V__Process2) = V__Time2) & s__starts(V__Time2,V__Time) & (s__WhenFn(V__Process1) = V__Time1) & (s__EndFn(V__Time) = s__BeginFn(V__Time1)))))) => (s__duration(V__Time,V__Delay))))) ) )	QoSontology.kif 1259-1273	If there exist a time interval and another time interval such that a time duration is a dependency delay of a computer program and startup block is a dependency type of the computer program and another computer program has a dependency on the computer program and a computer process is an instance of computer process and the computer program is a program running of the computer process and another computer process is an instance of computer process and the other computer program is a program running of the other computer process and the time of existence of the other computer process is equal to the other time interval and the other time interval starts a third time interval and the time of existence of the computer process is equal to the time interval and the end of the third time interval is equal to the beginning of the time interval, then duration of the third time interval is the time duration

consequent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 11877-11884	A process is an instance of combining and an object is a resource for the process and an entity is a result of the process if and only if the object is not a part of the entity holds during the beginning of the time of existence of the process and the object is a part of the entity holds during the end of the time of existence of the process
( ! [V__TIME,V__PHYS] : ((s__instance(V__PHYS,s__Physical) => ((((s__time(V__PHYS,V__TIME) & s__instance(V__TIME,s__TimePoint)) => s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS)) ,V__TIME,s__EndFn(s__WhenFn(V__PHYS)))) & (s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS)) ,V__TIME,s__EndFn(s__WhenFn(V__PHYS))) => (s__time(V__PHYS,V__TIME) & s__instance(V__TIME,s__TimePoint)))))) ) )	Merge.kif 7934-7938	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
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__earlier(V__INTERVAL1,V__INTERVAL2) => s__before(s__EndFn(V__INTERVAL1) ,s__BeginFn(V__INTERVAL2))) & (s__before(s__EndFn(V__INTERVAL1) ,s__BeginFn(V__INTERVAL2)) => s__earlier(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 8028-8030	A time interval happens earlier than another time interval if and only if the end of the time interval happens before the beginning of the other time interval
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__finishes(V__INTERVAL1,V__INTERVAL2) => (s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1)) & (s__EndFn(V__INTERVAL2) = s__EndFn(V__INTERVAL1)))) & ((s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1)) & (s__EndFn(V__INTERVAL2) = s__EndFn(V__INTERVAL1))) => s__finishes(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 7832-7840	A time interval finishes another time interval if and only if the beginning of the other time interval happens before the beginning of the time interval and the end of the other time interval is equal to the end of the time interval
( ! [V__PROCESS] : (((s__instance(V__PROCESS,s__Creation) => ( ? [V__PATIENT] : ((s__instance(V__PATIENT,s__Physical) & (s__patient(V__PROCESS,V__PATIENT) & s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS))) & ~(s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS))))))))) & (( ? [V__PATIENT] : ((s__instance(V__PATIENT,s__Physical) & (s__patient(V__PROCESS,V__PATIENT) & s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS))) & ~(s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS)))))))) => s__instance(V__PROCESS,s__Creation))) ) )	Merge.kif 12194-12201	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
( ! [V__PROCESS] : (((s__instance(V__PROCESS,s__Destruction) => ( ? [V__PATIENT] : ((s__instance(V__PATIENT,s__Physical) & (s__patient(V__PROCESS,V__PATIENT) & s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS))) & ~(s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS))))))))) & (( ? [V__PATIENT] : ((s__instance(V__PATIENT,s__Physical) & (s__patient(V__PROCESS,V__PATIENT) & s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS))) & ~(s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS)))))))) => s__instance(V__PROCESS,s__Destruction))) ) )	Merge.kif 11701-11708	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
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__meetsTemporally(V__INTERVAL1,V__INTERVAL2) => (s__EndFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2))) & ((s__EndFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) => s__meetsTemporally(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 7998-8002	A time interval meets another time interval if and only if the end of the time interval is equal to the beginning of the other time interval
( ! [V__INTERVAL2,V__INTERVAL1] : (((s__instance(V__INTERVAL2,s__TimeInterval) & s__instance(V__INTERVAL1,s__TimeInterval)) => (((s__starts(V__INTERVAL1,V__INTERVAL2) => ((s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2)))) & (((s__BeginFn(V__INTERVAL1) = s__BeginFn(V__INTERVAL2)) & s__before(s__EndFn(V__INTERVAL1) ,s__EndFn(V__INTERVAL2))) => s__starts(V__INTERVAL1,V__INTERVAL2))))) ) )	Merge.kif 7810-7818	A time interval starts another time interval if and only if the beginning of the time interval is equal to the beginning of the other time interval and the end of the time interval happens before the end of the other time interval
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 615-627	If a financial account amount due a currency measure for a time position and a cognitive agent holds account the financial account, then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
( ! [V__DAY,V__Y1,V__Y2] : (((s__instance(V__DAY,s__Day) & s__instance(V__Y1,s__TimeInterval) & s__instance(V__Y2,s__TimeInterval)) => (((s__birthdate(s__JesusOfNazareth,V__DAY) & s__instance(V__Y1,s__YearFn(n___6)) & s__instance(V__Y2,s__YearFn(n__4))) => (s__temporalPart(V__DAY,s__TimeIntervalFn(s__BeginFn(V__Y1) ,s__EndFn(V__Y2))))))) ) )	Media.kif 1938-1943	If a day is a birthdate of JesusOfNazareth and a time interval is an instance of the year -6 and another time interval is an instance of the year 4, then the day is a part of interval between the beginning of the time interval and the end of the other time interval
( ! [V__DAY,V__Y1,V__Y2] : (((s__instance(V__DAY,s__Day) & s__instance(V__Y1,s__TimeInterval) & s__instance(V__Y2,s__TimeInterval)) => (((s__deathdate(s__JesusOfNazareth,V__DAY) & s__instance(V__Y1,s__YearFn(n__29)) & s__instance(V__Y2,s__YearFn(n__36))) => (s__temporalPart(V__DAY,s__TimeIntervalFn(s__BeginFn(V__Y1) ,s__EndFn(V__Y2))))))) ) )	Media.kif 1945-1950	If a day is a deathdate of JesusOfNazareth and a time interval is an instance of the year 29 and another time interval is an instance of the year 36, then the day is a part of interval between the beginning of the time interval and the end of the other time interval
( ! [V__TEXT,V__EDITION1,V__CBO2,V__EDITION2,V__CBO1,V__INT2,V__PUB2,V__DATE1,V__INT1,V__DATE2,V__PUB1] : (((s__subclass(V__TEXT,s__ContentBearingObject) & s__subclass(V__EDITION1,s__ContentBearingObject) & s__instance(V__EDITION1,s__Class) & s__subclass(V__EDITION2,s__ContentBearingObject) & s__instance(V__EDITION2,s__Class) & s__instance(V__INT2,s__PositiveInteger) & s__instance(V__DATE1,s__Day) & s__instance(V__INT1,s__PositiveInteger) & s__instance(V__DATE2,s__Day)) => ((((s__EditionFn(V__TEXT,V__INT1) = V__EDITION1) & (s__EditionFn(V__TEXT,V__INT2) = V__EDITION2) & s__greaterThan(V__INT2,V__INT1) & s__instance(V__PUB1,s__Publication) & s__instance(V__PUB2,s__Publication) & s__instance(V__CBO1,V__EDITION1) & s__instance(V__CBO2,V__EDITION2) & s__patient(V__PUB1,V__CBO1) & s__patient(V__PUB2,V__CBO2) & s__date(V__PUB1,V__DATE1) & s__date(V__PUB2,V__DATE2)) => (s__before(s__EndFn(V__DATE1) ,s__EndFn(V__DATE2)))))) ) )	Merge.kif 14846-14863	If edition a positive integer of a kind of content bearing object is equal to another kind of content bearing object and edition another positive integer of a kind of content bearing object is equal to a third kind of content bearing object and the other positive integer is greater than the positive integer and a process is an instance of publication and another process is an instance of publication and an entity is an instance of another kind of content bearing object and another entity is an instance of a third kind of content bearing object and the entity is a patient of the process and the other entity is a patient of the other process and date of the process is a day and date of the other process is another day, then the end of the day happens before the end of the other day
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 20457-20468	If a process is an instance of aborting and an entity is a patient of the process and the entity is an instance of woman, then pregnant is an attribute of the entity holds during the beginning of the time of existence of the process and pregnant is not an attribute of the entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16244-16265	If a process is an instance of accelerating and an agent is an agent of the process, then there exist a quantity, another quantity,, , a third quantity,, , a fourth quantity,, , an entity and another entity such that the measure of the agent is the quantity the entity(s) per the third quantity the other entity(s) holds during the beginning of the time of existence of the process and the measure of the agent is the other quantity the entity(s) per the fourth quantity the other entity(s) holds during the end of the time of existence of the process and the other quantity is greater than the quantity or the fourth quantity is greater than the third quantity
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 2297-2306	If a process is an instance of ActivatingUIElement and an entity is a patient of the process and the entity is an instance of GUIElement, then the entity has state GUE_ActiveState holds during the end of a time interval and not the entity has state GUE_ActiveState holds during the start of the time interval
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 2361-2372	If a time interval is an instance of BringingGEToFront and an entity is a patient of the time interval and the entity is an instance of InterfaceWindow and the entity has state an attribute holds during the beginning of the time interval and the attribute is the opposite of GUE_UncoveredState, then not the entity has state the attribute holds during the end of the time interval
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 2376-2383	If a time interval is an instance of BringingGEToFront and an entity is a patient of the time interval and the entity is an instance of InterfaceWindow, then the entity has state GUE_UncoveredState holds during the end of the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12056-12069	If a process is an instance of shape change and an entity is a patient of the process, then there exists another entity such that the other entity is an instance of shape attribute and the other entity is an attribute of the entity holds during the beginning of the time of existence of the process and the other entity is not an attribute of the entity holds during the end of the time of existence of the process or the other entity is not an attribute of the entity holds during the beginning of the time of existence of the process and the other entity is an attribute of the entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12016-12029	If a process is an instance of surface change and an object is a patient of the process, then there exist another object and an entity such that the other object is a superficial part of the object and the entity is an attribute of the other object holds during the beginning of the time of existence of the process and the entity is not an attribute of the other object holds during the end of the time of existence of the process or the entity is not an attribute of the other object holds during the beginning of the time of existence of the process and the entity is an attribute of the other object holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 1523-1539	If a time interval is an instance of add to cart and an entity is an instance of object and the entity is a patient of the time interval and an agent is an agent of the time interval, then there exist a collection, a WebSite and a time position such that the collection is an instance of collection and the WebSite is an instance of WebSite and another time interval is an instance of time interval and user the agent at the WebSite has cart the collection and the beginning of the other time interval is equal to the end of the time interval and the entity is a member of the collection holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11771-11778	If a process is an instance of attaching and an entity is a patient of the process and another entity is a patient of the process, then the entity is not connected to the other entity holds during the beginning of the time of existence of the process and the entity is connected to the other entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 15485-15495	If a process is an instance of becoming drunk and an agent experiences the process, then sober is an attribute of the agent holds during the beginning of the time of existence of the process and drunk is an attribute of the agent holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16485-16496	If a process is an instance of boarding and an agent is an agent of the process and an entity is a patient of the process, then not the agent is onboard the entity holds during the beginning of the time of existence of the process and the agent is onboard the entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16526-16538	If a process is an instance of deboarding and an agent is an agent of the process and an entity is a patient of the process, then the agent is onboard the entity holds during the beginning of the time of existence of the process and not the agent is onboard the entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 15505-15515	If a process is an instance of sobering up and an agent experiences the process, then drunk is an attribute of the agent holds during the beginning of the time of existence of the process and sober is an attribute of the agent holds during the end of the time of existence of the process

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

(s__EndFn(s__CommonEra) = s__PositiveInfinity)

Mid-level-ontology.kif 7542-7542

The end of common era is equal to positive infinity

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

KB Term:			Term intersection

English Word: