TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2707-2708
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8140-8141
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1430-1431
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8137-8137	The number 1 argument of before is an instance of time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8138-8138	The number 2 argument of before is an instance of time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8133-8133	before is an instance of irreflexive relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8132-8132	before is an instance of temporal relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8134-8134	before is an instance of transitive relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8136-8136	before is internally related to earlier
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8135-8135	before is a subrelation of before or equal

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 423-423
No TPTP formula. May not be expressible in strict first order.	english_format.kif 429-429
No TPTP formula. May not be expressible in strict first order.	french_format.kif 246-246
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 32-32
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2040-2040
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 198-198
No TPTP formula. May not be expressible in strict first order.	relations-cb.txt 66-66
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 251-251
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 550-550
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 76-76
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 267-267
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 267-267
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 80-80
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 424-424
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 10534-10534
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 10533-10533
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 81-81

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 8122-8130	If the beginning of a time interval happens before the beginning of another time interval and the end of the time interval is equal to the end of the other time interval, then the other time interval finishes the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8212-8216	If a time point happens before another time point and the other time point happens before a third time point, then the other time point is between the time point and the third time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8090-8098	If the beginning of a time interval is equal to the beginning of another time interval and the end of the time interval happens before the end of the other time interval, then the time interval starts the other time interval
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 494-507	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.	FinancialOntology.kif 1087-1099	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.	Weather.kif 1581-1591	If a process is an instance of flooding and an object is an instance of land area and the process is located at the object and a time point is an instance of time point and the time point happens before the time of existence of the process, then the statement the object is an instance of submerged land area holds during the time point has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 1496-1518	If a time interval is an instance of the time interval_CLASS and the time interval_CLASS is a subclass of process and an accessing web page is an instance of accessing web page 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 accessing web page and the time interval takes place during the accessing web page 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 accessing web page 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 accessing web page 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 accessing web page in the class the time interval_CLASS is equal to the physical
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8305-8315	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 other time interval happens before or at the beginning of the time interval and the beginning of the time interval happens before the end of the other time interval, then the time interval overlaps the other time interval
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2669-2685	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 2623-2639	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 2687-2703	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 2641-2659	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.	FinancialOntology.kif 834-842	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
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8418-8420	If the end of a time interval happens before the beginning of another time interval, then the time interval happens earlier than the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8187-8191	If a time point happens before another time point or the time point is equal to the other time point, then the time point happens before or at the other time point

consequent

No TPTP formula. May not be expressible in strict first order.	Music.kif 261-270	If an album was released on a time point, then there exist a geographic area and a kind of data storage device such that the set of copies on a kind of data storage device of the album was released for sale in the geographic area at the time point and there don't exist another time point, another geographic area and another kind of data storage device such that the other time point happens before the time point and the set of copies on another kind of data storage device of the album was released for sale in the other geographic area at the other time point
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6225-6238	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 substanceUB meets the human holds during a time position, then the statement there exists another entity such that the other entity is an instance of allergic reaction 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
No TPTP formula. May not be expressible in strict first order.	Music.kif 457-470	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
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 684-695	If one must check out before a time point at a cognitive agent and another cognitive agent is a guest at the cognitive agent, then the cognitive agent expects there exist an entity and another entity such that the entity is an instance of the time point and the other cognitive agent is a patient of the other entity and the other entity is an instance of check-out service and the cognitive agent is an agent of the other entity and the beginning of the time of existence of the other entity happens before the entity will be true
No TPTP formula. May not be expressible in strict first order.	Communications.kif 202-214	If a process ends up at an object and the process is an instance of messaging and an entity is a patient of the process and the object is an instance of telex, then there exist another process and another entity such that the object is an instrument for the other process and the other entity is a result of the other process and the other entity expresses the entity and the other entity is an instance of text and the beginning of the time of existence of the process happens before the beginning of the time of existence of the other process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8317-8324	If a time interval happens earlier than another time interval and a time point is an instance of time point and another time point is an instance of time point and the time point is a part of the time interval and the other time point is a part of the other time interval, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15561-15578	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 22972-22977	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
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 29646-29655	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 8758-8765	If a time interval is an instance of the day a positive integer and another time interval is an instance of the day another positive integer and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and the other positive integer is greater than the positive integer, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1615-1624	If a financial account is an instance of interest only loan and a time interval is an agreement period of the financial account and a currency measure is a principal amount of the financial account and the financial account is interest earned an interest for the time interval, then the financial account amount due the currency measure for the end of the time interval and the financial account amount due the interest for another time interval and the end of the other time interval happens before the end of the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8742-8749	If a time interval is an instance of the month a kind of month and another time interval is an instance of the month another kind of month and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and another kind of month is the successor class of a kind of month., then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7923-7927	If a time point is an instance of time point and the time point is not equal to negative infinity, then negative infinity happens before the time point
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7905-7909	If a time point is an instance of time point and the time point is not equal to positive infinity, then the time point happens before positive infinity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12209-12218	If a process is an instance of remembering and a formula is a patient of the process, then there exists a time interval such that the formula holds during the time interval and the time interval happens before the time of existence of the process or the time interval happens earlier than the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Geography.kif 2328-2338	If a process is an instance of aftershock and the process is located at an object, then there exists another process such that the other process is an instance of earth tremor and the other process is located at the object and the time of existence of the other process happens before the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8298-8303	If a time interval is an instance of time interval and a time point is equal to the beginning of the time interval and another time point is equal to the end of the time interval, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	Dining.kif 274-291	If a collection is an instance of buffet and a physical is a member of the collection and the collection is located at an object and a process is an instance of eating and an agent is an agent of the process and the process is located at another object and the physical is a patient of the process, then the object is not equal to the other object and there exists another process such that the other process is an instance of getting and the physical is a patient of the other process and the other process originates at the object and the agent is an agent of the other process and the time of existence of the other process happens before the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 27006-27032	If a physical is an instance of surveillance system and the physical is a member of a collection and the physical is a member of another collection and the collection is located at an object and the collection is an instance of camera and the other collection is located at another object and the object is not equal to the other object and the other collection is an instance of video display, then the physical has the purpose there exist an entity, another entity,, , a third entity and a fourth entity such that the entity is an instance of process and the entity is located at the object and the other entity expresses the entity and camera is an instrument for the fourth entity and the other entity is a result of the fourth entity and the third entity is an instance of radiating light and the other collection is an instrument for the third entity and the other entity is a patient of the third entity and the beginning of the entity happens before the beginning of the fourth entity and the beginning of the fourth entity happens before the beginning of the third entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8726-8733	If a time interval is an instance of the year an integer and another time interval is an instance of the year another integer and a time point is equal to the beginning of the time interval and another time point is equal to the beginning of the other time interval and the other integer is greater than the integer, then the time point happens before the other time point
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2788-2800	If an agreement the attribute american style option and a cognitive agent holds the agreement and the agreement has expiration a time point, then the cognitive agent has the right to perform there exists an entity such that the entity is an instance of exercise an option and the agreement is a patient of the entity and the end of the time of existence of the entity happens before the end of the time point
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14651-14665	If a kind of series is a subclass of periodical and volume a positive integer in the series a kind of series is equal to a kind of text and volume another positive integer in the series the kind of series is equal to another kind of text 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 a kind of text and another entity is an instance of another kind of text 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.	Merge.kif 8181-8185	If a time point happens before or at another time point, then the time point happens before the other time point or the time point is equal to the other time point
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 4317-4321	If an experimenting takes a time interval to burn in, then the end of the time interval happens before the end of the time of existence of the experimenting
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 667-675	If an organization allows checkins after a kind of time point, then the statement there exist an entity and another entity such that the entity is an instance of a kind of time point and the other entity is an instance of check-in service and the organization is an agent of the other entity and the beginning of the time of existence of the other entity happens before the entity has the modal force of unlikely

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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

KB Term:			Term intersection

English Word: