WhenFn - Sigma Knowledge base Browser

appearance as argument number 1

s__documentation(s__WhenFn__m,s__ChineseLanguage,'"这是一个 UnaryFunction，它把一个 Object 或 Process 联系到它存在的准确 TimeInterval。注：在 TimeInterval (WhenFn ?THING)以外的每一个 TimePoint ?TIME， (time ?THING ?TIME) 并不存在"')	chinese_format.kif 2736-2738
s__documentation(s__WhenFn__m,s__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 7897-7900
s__domain(s__WhenFn__m,n__1,s__Physical)	Merge.kif 7894-7894	The number 1 argument of when is an instance of physical
s__instance(s__WhenFn__m,s__TemporalRelation) s__instance(s__TemporalRelation,s__SetOrClass)	Merge.kif 7891-7891	When is an instance of temporal relation
s__instance(s__TotalValuedRelation,s__SetOrClass) s__instance(s__WhenFn__m,s__TotalValuedRelation)	Merge.kif 7893-7893	When is an instance of total valued relation
s__instance(s__UnaryFunction,s__SetOrClass) s__instance(s__WhenFn__m,s__UnaryFunction)	Merge.kif 7892-7892	When is an instance of unary function
s__range(s__WhenFn__m,s__TimeInterval)	Merge.kif 7895-7895	The range of when is an instance of time interval

appearance as argument number 2

s__format(s__ChineseLanguage,s__WhenFn__m,'"%1 出现的 time"')	chinese_format.kif 455-455
s__format(s__EnglishLanguage,s__WhenFn__m,'"the time of existence of %1"')	english_format.kif 464-464
s__relatedInternalConcept(s__WhereFn__m,s__WhenFn__m)	Merge.kif 4042-4042	Where is internally related to when
s__termFormat(s__ChineseLanguage,s__WhenFn__m,'"何时"')	domainEnglishFormat.kif 62872-62872
s__termFormat(s__ChineseLanguage,s__WhenFn__m,'"何时函数"')	chinese_format.kif 456-456
s__termFormat(s__ChineseTraditionalLanguage,s__WhenFn__m,'"何時"')	domainEnglishFormat.kif 62871-62871
s__termFormat(s__EnglishLanguage,s__WhenFn__m,'"when"')	domainEnglishFormat.kif 62870-62870

antecedent

( ! [V__POS,V__THING] : ((s__instance(V__POS,s__TimePosition) & s__instance(V__THING,s__Physical)) => (s__temporalPart(V__POS,s__WhenFn(V__THING)) => s__time(V__THING,V__POS)) & (s__time(V__THING,V__POS) => s__temporalPart(V__POS,s__WhenFn(V__THING))) ) )	Merge.kif 7528-7530	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
No TPTP formula. May not be expressible in strict first order.	Cars.kif 2572-2588	If the idle speed of an internal combustion engine is the rotation of a rotating during a time duration and an object is an instance of automobile and a process is an instance of gas pedal and the process is an instance of pushing and the process ends up at another object and the internal combustion engine is a part of the object and the other object is a part of the object and a third object is an instance of Crankshaft and the third object is a part of the internal combustion engine and the measure of the third object is the rotation of an entity during the time duration holds during the time of existence of the process, then the statement the entity is greater than the rotating has the modal force of likely
( ! [V__AGENT,V__PROCESS_START,V__PROCESS,V__AGENT_END] : ((s__instance(V__AGENT,s__Agent) & s__instance(V__PROCESS_START,s__TimePoint) & s__instance(V__PROCESS,s__Process) & s__instance(V__AGENT_END,s__TimePoint)) => ((V__PROCESS_START = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENT_END = s__EndFn(s__WhenFn(V__AGENT))) & s__benefits(V__PROCESS,V__AGENT)) => s__before(V__PROCESS_START,V__AGENT_END) ) )	Mid-level-ontology.kif 20816-20821	If a process-START is equal to the beginning of the time of existence of the process and an agent-END is equal to the end of the time of existence of the agent and the agent is a beneficiary of the process, then the process-START happens before the agent-END
( ! [V__AGENT,V__PROCESS_START,V__PROCESS,V__AGENT_END] : ((s__instance(V__AGENT,s__Agent) & s__instance(V__PROCESS_START,s__TimePoint) & s__instance(V__PROCESS,s__Process) & s__instance(V__AGENT_END,s__TimePoint)) => ((V__PROCESS_START = s__BeginFn(s__WhenFn(V__PROCESS))) & (V__AGENT_END = s__EndFn(s__WhenFn(V__AGENT))) & s__suffers(V__PROCESS,V__AGENT)) => s__before(V__PROCESS_START,V__AGENT_END) ) )	Mid-level-ontology.kif 27770-27779	If a process-START is equal to the beginning of the time of existence of the process and an agent-END is equal to the end of the time of existence of the agent and the agent suffers from the process, then the process-START happens before the agent-END
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3219-3233	If booting up is an attribute of an engineering component holds during a physical and host ready is an attribute of the engineering component holds during the physical2 and the physical2 is equal to immediately after the time of existence of the physical and another engineering component is an instance of ComputerDisplay and the other engineering component is connected to the engineering component, then the statement there exists an entity such that the entity is an instance of home screen and the entity is displayed on the other engineering component has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	Law.kif 524-533	If an agent desires dead is an attribute of an entity holds during a time interval and the agentURDER is an instance of murder and the agent is an agent of the agentURDER and the entity is a patient of the agentURDER and the time interval happens earlier than the time of existence of the agentURDER, then premeditated is an attribute of the agentURDER
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 28807-28828	If dieting is an attribute of an agent holds during a time interval and dieting is not an attribute of the agent holds during another time interval and an object is an instance of meal and a process is an instance of eating and the agent is an agent of the process and the object is a resource for the process and the time of existence of the process takes place during the time interval and the measure of the object is a real number calorie(s) and another object is an instance of meal and another process is an instance of eating and the agent is an agent of the other process and the other object is a resource for the other process and the time of existence of the other process takes place during the other time interval and the measure of the other object is another real number calorie(s), then the statement the other real number is greater than the real number has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16864-16870	If embryonic is an attribute of an agent holds during a time interval and a process is an instance of birth and another time interval is equal to the time of existence of the process and the agent experiences the process, then the other time interval doesn't overlap the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16835-16841	If larval is an attribute of an agent holds during a time interval and a process is an instance of birth and another time interval is equal to the time of existence of the process and the agent experiences the process, then the other time interval meets the time interval
( ! [V__A,V__T,V__E] : ((s__instance(V__T,s__TimeInterval) & s__instance(V__E,s__Agent)) => (s__instance(V__A,s__Accelerating) & (V__T = s__WhenFn(V__A)) & s__experiencer(V__A,V__E)) => ~(( ? [V__D] : ((s__instance(V__D,s__Decelerating) & s__experiencer(V__D,V__E) & (V__T = s__WhenFn(V__D)))))) ) )	Mid-level-ontology.kif 14760-14770	If a process is an instance of accelerating and a time interval is equal to the time of existence of the process and an agent experiences the process, then there doesn't exist another process such that the other process is an instance of decelerating and the agent experiences the other process and the time interval is equal to the time of existence of the other process
( ! [V__S2_START,V__A,V__S1,V__S2,V__S1_START] : ((s__instance(V__S2_START,s__TimePoint) & s__instance(V__S1_START,s__TimePoint)) => (s__instance(V__A,s__Ambulating) & s__subProcess(V__S1,V__A) & s__instance(V__S1,s__Stepping) & s__subProcess(V__S2,V__A) & s__instance(V__S2,s__Stepping) & (V__S1_START = s__BeginFn(s__WhenFn(V__S1))) & (V__S2_START = s__BeginFn(s__WhenFn(V__S2))) & ~((s__before(V__S1_START,V__S2_START) \| s__before(V__S2_START,V__S1_START)))) => (V__S1 = V__S2) ) )	Mid-level-ontology.kif 675-688	If a process is an instance of ambulating and another process is a subprocess of the process and the other process is an instance of stepping and a third process is a subprocess of the process and the third process is an instance of stepping and the other process-START is equal to the beginning of the time of existence of the other process and the third process-START is equal to the beginning of the time of existence of the third process and the other process-START happens before the third process-START and the third process-START happens before the other process-START, then the other process is equal to the third process
( ! [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 3961-3986	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__AMBULATE,V__DURATION] : (s__instance(V__DURATION,s__TimeInterval) => (s__instance(V__AMBULATE,s__Ambulating) & (V__DURATION = s__WhenFn(V__AMBULATE))) => ( ? [V__STEP1, V__STEPN] : ((s__instance(V__STEP1,s__Stepping) & s__instance(V__STEPN,s__Stepping) & s__subProcess(V__STEP1,V__AMBULATE) & s__subProcess(V__STEPN,V__AMBULATE) & s__starts(s__WhenFn(V__STEP1) ,V__DURATION) & s__finishes(s__WhenFn(V__STEPN) ,V__DURATION) & ~((V__STEP1 = V__STEPN))))) ) )	Mid-level-ontology.kif 660-672	If a process is an instance of ambulating and a time interval is equal to the time of existence of the process, then there exist another process and a third process such that the other process is an instance of stepping and the third process is an instance of stepping and the other process is a subprocess of the process and the third process is a subprocess of the process and the time of existence of the other process starts the time interval and the time of existence of the third process finishes the time interval and the other process is not equal to the third process
No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 89-103	If a process is an instance of armed reconnaissance and a cognitive agent is an agent of the process and an entity is a patient of the process and the cognitive agent and the entity are enemies of each other holds during the time of existence of the process, then the process allows the cognitive agent to perform task of the type there exists another entity such that the other entity is an instance of attack and the cognitive agent is an agent of the other entity and the entity is a patient of the other entity
No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 665-671	If a process is an instance of anti surface operation and an entity is a patient of the process and the entity is located at another entity holds during the time of existence of the process, then the other entity is an instance of water area
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12790-12798	If a process is an instance of boiling and a real number an unit of measure(s) is a boiling point of a kind of pure substance and an entity is an instance of a kind of pure substance and the entity is a patient of the process and the measure of the entity is a quantity the unit of measure(s) holds during the time of existence of the process and the unit of measure is an instance of UnitOfTemperature, then the quantity is greater than or equal to the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10837-10844	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
( ! [V__AGENT,V__TIME,V__SITE,V__LISTING,V__COLL] : ((s__instance(V__COLL,s__Collection) & s__instance(V__SITE,s__WebSite) & s__instance(V__AGENT,s__Agent) & s__instance(V__LISTING,s__WebListing) & s__instance(V__TIME,s__TimePoint) & s__listingSeller(V__LISTING,V__AGENT) & ~(s__member(V__LISTING,V__COLL)) & ( ! [V__ITEM] : ((s__instance(V__ITEM,s__WebListing) & s__member(V__ITEM,s__SellersItemsFn(V__AGENT,V__SITE)) & s__temporalPart(V__TIME,s__WhenFn(V__ITEM)) & ~((V__ITEM = V__LISTING))) => s__member(V__ITEM,V__COLL))) & ( ! [V__MEMBER] : (s__member(V__MEMBER,V__COLL) => (s__temporalPart(V__TIME,s__WhenFn(V__ITEM)) & s__instance(V__MEMBER,s__WebListing))))) => (s__SellersOtherItemsFn(V__AGENT,V__SITE,V__LISTING,V__TIME) = V__COLL) ) )	UXExperimentalTerms.kif 1226-1253	If a collection is an instance of collection and a WebSite is an instance of WebSite and an agent is an instance of agent and a web listing is an instance of web listing and a time point is an instance of time point and the agent sells the web listing and the web listing is not a member of the collection and for all an object if the object is an instance of web listing and the object is a member of items for sale by the agent at the WebSite and the time point is a part of the time of existence of the object and the object is not equal to the web listing, then the object is a member of the collection and for all another object if the other object is a member of the collection, then the time point is a part of the time of existence of the object and the other object is an instance of web listing , then things for sale by the agent not listed in the web listing at the WebSite during the time point is equal to the collection
No TPTP formula. May not be expressible in strict first order.	Government.kif 761-769	If a proposition is an instance of the constitution of a geopolitical area and the geopolitical area is an instance of nation and a government is equal to the geopolitical area の government and the time of existence of the government is an agreement effective during of the proposition and another proposition is a sub-proposition of the proposition and a formula contains information the other proposition, then the government is obliged to perform tasks of type the formula
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1932-1946	If a computer process is an instance of data compression and a digital data is processed by the computer process and the digital data requires a quantity an entity(s) holds during immediately before the time of existence of the computer process and the digital data requires another quantity the entity(s) holds during immediately after the time of existence of the computer process, then the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4491-4501	If a process is an instance of deleting an account and an entity is an instance of account and an agent has account the entity holds during immediately before the time of existence of the process and the entity is a patient of the process and the agent is an agent of the process, then not the agent has account the entity holds during immediately after the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 609-622	If a process is an instance of dodging and an agent is an agent of the process and the processT is equal to the time of existence of the process, then the process purpose there doesn't exist an entity such that the processT meets the time of existence of the entity or the time of existence of the entity overlaps the processT and the entity is an instance of impacting and the agent is a patient of the entity
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6354-6368	If a process is an instance of deposition and an entity is a patient of the process and the measure of the entity is a quantity joule(s) holds during immediately before the time of existence of the process and the measure of the entity is another quantity joule(s) holds during immediately after the time of existence of the process, then the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11137-11146	If a process is an instance of discovering and an entity is a patient of the process and the entity is located at another entity holds during the time of existence of the process, then there exists another process such that the other process is an instance of learning and the other process is a subprocess of the process and the entity is located at the other entity is a patient of the other process
( ! [V__Amount,V__Balance2,V__Balance1,V__Deposit,V__Account] : ((s__instance(V__Amount,s__CurrencyMeasure) & s__instance(V__Balance2,s__CurrencyMeasure) & s__instance(V__Balance1,s__CurrencyMeasure)) => (s__instance(V__Deposit,s__Deposit) & s__instance(V__Account,s__FinancialAccount) & s__destination(V__Deposit,s__CurrencyFn(V__Account)) & s__transactionAmount(V__Deposit,V__Amount) & s__currentAccountBalance(V__Account,s__ImmediatePastFn(s__WhenFn(V__Deposit)) ,V__Balance1) & (V__Balance2 = s__AdditionFn(V__Balance1,V__Amount))) => s__currentAccountBalance(V__Account,s__ImmediateFutureFn(s__FutureFn(V__Deposit)) ,V__Balance2) ) )	FinancialOntology.kif 428-436	If a financial transaction is an instance of deposit and a financial account is an instance of financial account and the financial transaction ends up at the currency of the financial account and a currency measure is a transaction amount of the financial transaction and the financial account current account balance immediately before the time of existence of the financial transaction for another currency measure and a third currency measure is equal to (the other currency measure and the currency measure), then the financial account current account balance immediately after after the financial transaction for the third currency measure

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 11520-11527	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 7721-7725	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__PHYS1,V__PHYS2] : ((s__instance(V__PHYS1,s__Physical) & s__instance(V__PHYS2,s__Physical)) => (s__cooccur(V__PHYS1,V__PHYS2) => (s__WhenFn(V__PHYS1) = s__WhenFn(V__PHYS2))) & ((s__WhenFn(V__PHYS1) = s__WhenFn(V__PHYS2)) => s__cooccur(V__PHYS1,V__PHYS2)) ) )	Merge.kif 7828-7830	A physical occurs at the same time as another physical if and only if the time of existence of the physical is equal to the time of existence of the other physical
No TPTP formula. May not be expressible in strict first order.	People.kif 104-117	The births per thousand of a geopolitical area and the year an integer is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to a quantity and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the quantity is equal to the real number
No TPTP formula. May not be expressible in strict first order.	People.kif 138-151	The deaths per thousand of a geopolitical area and the year an integer is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to a quantity and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the quantity is equal to the real number
No TPTP formula. May not be expressible in strict first order.	People.kif 253-277	The deaths per thousand live births of a geopolitical area and the year an integer is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to a quantity and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the quantity is equal to the real number
No TPTP formula. May not be expressible in strict first order.	People.kif 411-442	The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order.	People.kif 323-353	The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order.	People.kif 367-398	The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 28381-28394	Alone is an attribute of an entity holds during a time interval if and only if there don't exist the entity2 and a process such that the entity is not equal to the entity2 and the entity2 is an instance of agent and the process is an instance of social interaction and the time of existence of the process takes place during the time interval and the entity is an involved in event of the process and the entity2 is an involved in event of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 28427-28435	Mute is an attribute of an agent holds during a time interval if and only if there doesn't exist a process such that the process is an instance of speaking and the time of existence of the process takes place during the time interval and the agent is an agent of the process
( ! [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 11837-11844	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 11385-11392	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
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14409-14418	If a human's almaMater is a post secondary school, then there exists a process such that the process is an instance of educational process and the process ends up at the human and the process is located at 2 and student is an attribute of the human holds during the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18417-18424	If actedIn a human and a content bearing physical and a process is an instance of dramatic acting and the human is a patient of the process and the content bearing physical is a result of the process, then Actor is an attribute of the human holds during the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16510-16516	If an agent is an agent of a process and an entity is a result of the process and the entity is an instance of art work, then Artist is an attribute of the agent holds during the time of existence of the process
( ! [V__AC,V__A,V__T] : ((s__instance(V__AC,s__UserAccount) & s__instance(V__A,s__Agent) & s__instance(V__T,s__TimeInterval)) => (s__attribute(V__AC,s__TwoFactorAuthentication) & s__loggedInDuring(V__A,V__AC,V__T)) => ( ? [V__TF] : ((s__instance(V__TF,s__TwoFactorLoggingIn) & s__agent(V__TF,V__A) & s__accountUsed(V__TF,V__AC) & s__earlier(s__WhenFn(V__TF) ,V__T)))) ) )	ComputingBrands.kif 4298-4307	If two-factor authentication is an attribute of an user account and an agent is logged-in to the user account during a time interval, then there exists the time intervalF such that the time intervalF is an instance of two-factor login and the agent is an agent of the time intervalF and the accountUsed in the time intervalF is the user account and the time of existence of the time intervalF happens earlier than the time interval
No TPTP formula. May not be expressible in strict first order.	ArabicCulture.kif 193-210	If muslim is an attribute of an agent and value of belongings of the agent is equal to a currency measure, then the statement there exist an entity and another entity such that the entity is an instance of zakat and a third entity is an instance of year and the third entity takes place during the time of existence of the agent and fully formed is an attribute of the agent holds during the third entity and the agent is an agent of the entity and the other entity is a patient of the entity and value of the other entity is a fourth entity and the fourth entity is greater than the currency measure and 0.025 has the modal force of obligation
( ! [V__A,V__MR,V__M,V__MM] : ((s__instance(V__A,s__CognitiveAgent) & s__instance(V__M,s__Music) & s__instance(V__MM,s__Physical)) => (s__attribute(V__MR,s__CoverRecording) & s__instance(V__MR,s__MusicRecording) & s__songArtist(V__MR,V__A) & s__musicInterpretation(V__MR,V__M) & s__record(V__MR,V__MM)) => ( ? [V__ORIG, V__ARTIST, V__MUSIC] : ((s__instance(V__ORIG,s__MusicRecording) & s__instance(V__ARTIST,s__CognitiveAgent) & s__instance(V__MUSIC,s__Physical) & (s__musicInterpretation(V__ORIG,V__M) & s__songArtist(V__ORIG,V__ARTIST) & ~((V__A = V__ARTIST)) & s__record(V__ORIG,V__MUSIC) & s__before(s__WhenFn(V__MUSIC) ,s__WhenFn(V__MM)))))) ) )	Music.kif 454-467	If cover recording is an attribute of a music recording and the music recording is an instance of music recording and a cognitive agent is the performer in the music recording and the music recording is a recording of a music and the music recording is a record of the musicM, then there exist another music recording, the cognitive agentRTIST and the musicUSIC such that the other music recording is a recording of the music and the cognitive agentRTIST is the performer in the other music recording and the cognitive agent is not equal to the cognitive agentRTIST and the other music recording is a record of the musicUSIC and the time of existence of the musicUSIC happens before the time of existence of the musicM
( ! [V__Order,V__Period] : ((s__instance(V__Order,s__Agreement) & s__instance(V__Order,s__Object) & s__instance(V__Period,s__TimeInterval)) => (s__attribute(V__Order,s__FOKOrder) & s__agreementPeriod(V__Order,V__Period)) => (( ? [V__Fill, V__Time1] : ((s__instance(V__Time1,s__TimeInterval) & (s__instance(V__Fill,s__FillingAnOrder) & s__patient(V__Fill,V__Order) & (s__WhenFn(V__Fill) = V__Time1) & s__starts(V__Time1,V__Period))))) \| ( ? [V__Kill, V__Time2] : ((s__instance(V__Time2,s__TimeInterval) & (s__instance(V__Kill,s__CancellingAnOrder) & s__patient(V__Kill,V__Order) & (s__WhenFn(V__Kill) = V__Time2) & s__starts(V__Time2,V__Period)))))) ) )	FinancialOntology.kif 2802-2818	If FOK order is an attribute of an agreement and a time interval is an agreement period of the agreement, then there exist a process and another time interval such that the process is an instance of filling an order and the agreement is a patient of the process and the time of existence of the process is equal to the other time interval and the other time interval starts the time interval or there exist another process and a third time interval such that the other process is an instance of cancelling an order and the agreement is a patient of the other process and the time of existence of the other process is equal to the third time interval and the third time interval starts the time interval
( ! [V__Order,V__Period,V__End,V__Time] : ((s__instance(V__Order,s__Agreement) & s__instance(V__Order,s__Object) & s__instance(V__Period,s__TimeInterval) & s__instance(V__End,s__TimeInterval) & s__instance(V__Time,s__TimeInterval)) => (s__attribute(V__Order,s__GTCOrder) & s__agreementPeriod(V__Order,V__Period)) => (( ? [V__Execute] : ((s__instance(V__Execute,s__FillingAnOrder) & s__patient(V__Execute,V__Order) & (s__WhenFn(V__Execute) = V__Time) & s__overlapsTemporally(V__Time,V__Period)))) \| ( ? [V__Cancel] : ((s__instance(V__Cancel,s__CancellingAnOrder) & s__patient(V__Cancel,V__Order) & (s__WhenFn(V__Cancel) = V__End) & s__finishes(V__End,V__Period))))) ) )	FinancialOntology.kif 2838-2854	If GTC order is an attribute of an agreement and a time interval is an agreement period of the agreement, then there exists a process such that the process is an instance of filling an order and the agreement is a patient of the process and the time of existence of the process is equal to another time interval and the time interval overlaps the other time interval or there exists another process such that the other process is an instance of cancelling an order and the agreement is a patient of the other process and the time of existence of the other process is equal to a third time interval and the third time interval finishes the time interval
( ! [V__Order,V__Period] : ((s__instance(V__Order,s__Agreement) & s__instance(V__Order,s__Object) & s__instance(V__Period,s__TimeInterval)) => (s__attribute(V__Order,s__IOCOrder) & s__agreementPeriod(V__Order,V__Period)) => (( ? [V__Fill, V__Time1] : ((s__instance(V__Time1,s__TimeInterval) & (s__instance(V__Fill,s__FillingAnOrder) & s__patient(V__Fill,V__Order) & (s__WhenFn(V__Fill) = V__Time1) & s__starts(V__Time1,V__Period))))) \| ( ? [V__Kill, V__Time2] : ((s__instance(V__Time2,s__TimeInterval) & (s__instance(V__Kill,s__CancellingAnOrder) & s__patient(V__Kill,V__Order) & (s__WhenFn(V__Kill) = V__Time2) & s__starts(V__Time2,V__Period)))))) ) )	FinancialOntology.kif 2775-2791	If IOC order is an attribute of an agreement and a time interval is an agreement period of the agreement, then there exist a process and another time interval such that the process is an instance of filling an order and the agreement is a patient of the process and the time of existence of the process is equal to the other time interval and the other time interval starts the time interval or there exist another process and a third time interval such that the other process is an instance of cancelling an order and the agreement is a patient of the other process and the time of existence of the other process is equal to the third time interval and the third time interval starts the time interval
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1945-1963	If limit order is an attribute of a financial transaction and an agreement is a party to agreement of the financial transaction and broker is an attribute of the agreement and the financial transaction is order for buying for a security and the measure of the security is a physical quantity and a currency measure is a limit price of the financial transaction and an agent asks for another currency measure for the security and the other currency measure is less than or equal to the currency measure, then the agreement 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 1965-1983	If limit order is an attribute of a financial transaction and an agreement is a party to agreement of the financial transaction and broker is an attribute of the agreement and the financial transaction is order for selling for a security and the measure of the security is a physical quantity and a currency measure is a limit price of the financial transaction and an agent bids another currency measure for the security and the other currency measure is greater than or equal to the currency measure, then the agreement 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.	Dining.kif 1154-1171	If communal is an attribute of an object and the object is an instance of table and a process is an instance of eating and an agent is an agent of the process and the agent is an instance of group of people and the process is located at 2, then the statement there exist an entity and another entity such that the other entity is an instance of eating and the entity is an agent of the other entity and the agent is not equal to the entity and the entity is an instance of group of people and the other entity is located at 2 and the time of existence of the process meets the time of existence of the other entity and the object is equal to the object2 has the modal force of possibility

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

No TPTP formula. May not be expressible in strict first order.	Media.kif 1972-1980	There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of JesusOfNazareth and the time interval starts the time of existence of TwelveApostles and for all an entity if the entity is a member of TwelveApostles holds during the time interval, then JesusOfNazareth is a friend of the entity holds during the time interval
No TPTP formula. May not be expressible in strict first order.	Media.kif 1922-1922	JesusOfNazareth is located at palestine holds during the time of existence of JesusOfNazareth

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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners

KB Term:			Term intersection

English Word: