TreeView 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 8080-8083
s__domain(s__WhenFn__m,n__1,s__Physical)	Merge.kif 8077-8077	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 8074-8074	When is an instance of temporal relation
s__instance(s__TotalValuedRelation,s__SetOrClass) s__instance(s__WhenFn__m,s__TotalValuedRelation)	Merge.kif 8076-8076	When is an instance of total valued relation
s__instance(s__UnaryFunction,s__SetOrClass) s__instance(s__WhenFn__m,s__UnaryFunction)	Merge.kif 8075-8075	When is an instance of unary function
s__range(s__WhenFn__m,s__TimeInterval)	Merge.kif 8078-8078	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 4088-4088	Where is internally related to when
s__termFormat(s__ChineseLanguage,s__WhenFn__m,'"何时"')	domainEnglishFormat.kif 62952-62952
s__termFormat(s__ChineseLanguage,s__WhenFn__m,'"何时函数"')	chinese_format.kif 456-456
s__termFormat(s__ChineseTraditionalLanguage,s__WhenFn__m,'"何時"')	domainEnglishFormat.kif 62951-62951
s__termFormat(s__EnglishLanguage,s__WhenFn__m,'"when"')	domainEnglishFormat.kif 62950-62950

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 7708-7710	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 2599-2617	If the idle speed of an internal combustion engine is the rotation of a real number miles per hour(s) 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 miles per hour(s) during the time duration holds during the time of existence of the process, then the statement the entity is greater than the real number has the modal force of likely
( ! [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 21392-21397	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 28021-28030	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.	ComputingBrands.kif 3205-3219	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 29077-29098	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 17385-17391	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 17356-17362	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 15676-15686	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__S1START,V__A,V__S1,V__S2START,V__S2] : (((s__instance(V__S1START,s__TimePoint) & s__instance(V__S2START,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__S1START = s__BeginFn(s__WhenFn(V__S1))) & (V__S2START = s__BeginFn(s__WhenFn(V__S2))) & ~((s__before(V__S1START,V__S2START) \| s__before(V__S2START,V__S1START)))) => ((V__S1 = V__S2))))) ) )	Mid-level-ontology.kif 472-485	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 processSTART is equal to the beginning of the time of existence of the other process and the third processSTART is equal to the beginning of the time of existence of the third process and the other processSTART happens before the third processSTART and the third processSTART happens before the other processSTART, then the other process is equal to the third process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 9030-9052	If an object is an instance of antacid and a motion is an instance of ingesting and an agent is an agent of the motion and the object moves during the motion and another object is an instance of stomach and the other object is a part of the agent and the other object contains a third object and the third object is an instance of fluid holds during immediately before the time of existence of the motion and the other object contains a fourth object and the fourth object is an instance of fluid holds during immediately after the time of existence of the motion and phMeasure the third object and an AcidityMeasure and phMeasure the fourth object and another AcidityMeasure, then the other AcidityMeasure is greater than the AcidityMeasure
No TPTP formula. May not be expressible in strict first order.	Merge.kif 11761-11775	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__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 458-470	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 13167-13175	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 11120-11127	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, V__MEMBER] : ((((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))) & (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 1230-1257	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 a physical and another physical if the physical is an instance of web listing and the physical 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 physical and the physical is not equal to the web listing, then the physical is a member of the collection and if the other physical is a member of the collection, then the time point is a part of the time of existence of the physical and the other physical 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 government of the geopolitical area 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 4537-4547	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.	Merge.kif 11809-11818	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.	Mid-level-ontology.kif 421-434	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 has the 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

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 11844-11851	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 7901-7905	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 8011-8013	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 number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the number 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 number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the number 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 number 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 number 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 28638-28651	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 28686-28694	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 12161-12168	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 11668-11675	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 15335-15344	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 19140-19147	If a human &actedIn 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 17252-17258	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
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 5793-5806	If allergic a human and a kind of substance and a kind of substanceUB is an instance of the kind of substance and the kind of substance meets the human holds during a time position, then the statement there exists another entity such that the other entity is an instance of AllergicReaction and the human experiences the other entity and the time of existence of the other entity overlaps the time position and the beginning of the time position happens before the beginning of the time of existence of the other entity has the modal force of likely
( ! [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 4344-4353	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-212	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, another entity and a third entity such that the entity is an instance of zakat and a fourth entity is an instance of year and the fourth entity takes place during the time of existence of the agent and fully formed is an attribute of the agent holds during the fourth 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 fifth entity the third entity(s) and the third entity is an instance of UnitOfCurrency and the fifth 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 2821-2837	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 2857-2873	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 2794-2810	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 1958-1979	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 real number an unit of measure(s) is a limit price of the financial transaction and the unit of measure is an instance of UnitOfCurrency and an agent asks for another real number the unit of measure(s) for the security and the other real number is less than or equal to the real number, 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 1981-2002	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 real number an unit of measure(s) is a limit price of the financial transaction and an agent bids another real number the unit of measure(s) for the security and the unit of measure is an instance of UnitOfCurrency and the other real number is greater than or equal to the real number, then the agreement is obliged to perform tasks of type the class described by a symbolic string

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 simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: