TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1973-1975
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3109-3111
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 605-607
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3106-3106	The number 1 argument of in list is an instance of entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3107-3107	The number 2 argument of in list is an instance of list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3104-3104	in list is an instance of binary predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3105-3105	in list is an instance of partial valued relation

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 131-131
No TPTP formula. May not be expressible in strict first order.	english_format.kif 132-132
No TPTP formula. May not be expressible in strict first order.	french_format.kif 87-87
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 147-147
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1914-1914
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 39-39
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 103-103
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 157-157
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 186-186
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 106-106
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 86-86
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 298-298
No TPTP formula. May not be expressible in strict first order.	Music.kif 332-332	album track is a subrelation of in list
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 30193-30193
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 132-132
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 30192-30192
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 30191-30191
No TPTP formula. May not be expressible in strict first order.	terms-de.txt 47-47
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 299-299

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 3286-3290	If a real number is equal to the average of the numbers in a list and an entity is a member of the list, then the entity is an instance of number
No TPTP formula. May not be expressible in strict first order.	Weather.kif 2005-2017	If a list is equal to Mean3SecondWindSpeedListFn ending at a time interval in region a geographic area and a function quantity is a member of the list, then there exist the time intervalLIST and another time interval such that the time intervalLIST is equal to ConsecutiveTimeIntervalList for at the time interval at 3 second duration(s) is contained in TimeIntervalListFn and the other time interval is a member of the time intervalLIST and the function quantity is equal to Mean3SecondWindSpeedFn for the other time interval in region the geographic area
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1998-2003	If a list is equal to Mean3SecondWindSpeedListFn ending at a time interval in region a geographic area and an entity is a member of the list, then the entity is an instance of function quantity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 503-507	If @ROW are all the attributes of another kind of attribute and an entity is a member of (@ROW), then the entity is an instance of another kind of attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 497-501	If @ROW are all the attributes of another kind of attribute and an entity is a member of (@ROW), then the entity is an instance of attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7582-7587	If an entity is a member of a list and the list is equal to Amounts fn a kind of substance, a corpuscular object and an unit of mass, then the entity is an instance of rational number
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1975-1980	If a time interval is a member of a consecutive time interval list and the consecutive time interval list is equal to ConsecutiveTimeIntervalList for at another time interval at a time duration is contained in TimeIntervalListFn, then duration of the time interval is the time duration
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1966-1973	If an entity is a member of a consecutive time interval list and the consecutive time interval list is equal to ConsecutiveTimeIntervalList for at a time interval at a time duration is contained in TimeIntervalListFn, then the beginning of the time interval is equal to the beginning of the first of the consecutive time interval list
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2491-2498	If an entity is a member of a list and the list is an instance of search results, then there exists a corpuscular object such that the corpuscular object is an instance of search results page and the list is a component of the corpuscular object
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2483-2489	If an entity is a member of a list and the list is an instance of search results, then the entity is an instance of web listing or the entity is an instance of web page
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1929-1933	If a list is an instance of consecutive time interval list and an entity is a member of the list, then another entity is an instance of time interval
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1716-1720	If a list is an instance of measuring list and an entity is a member of the list, then the entity is an instance of measuring
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1784-1788	If a list is an instance of measuring result list and an entity is a member of the list, then the entity is an instance of physical quantity
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1750-1754	If a list is an instance of measuring surface wind speed list and an entity is a member of the list, then the entity is an instance of surface wind speed measuring
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1819-1823	If a list is an instance of number list and an entity is a member of the list, then the entity is an instance of number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2677-2682	If an entity is an instance of intentional relation and the entity a cognitive agent and @ROW and a third entity is a member of (@ROW), then the cognitive agent is interested in the third entity
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1769-1775	If The eventLocated for a measuring list is a geographic area and a process is a member of the measuring list, then the process is an instance of measuring and the process is located at the geographic area
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1860-1864	If The Measuring for list a measuring list occurs at a time duration interval. and a physical is a member of the measuring list, then duration of the time of existence of the physical is the time duration
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16921-16929	If an object is a positional attribute to another object and @ROW is the opposite of and the positional attribute is a member of (@ROW) and another positional attribute is a member of (@ROW) and the positional attribute is not equal to the other positional attribute, then the object is not the other positional attribute to the other object
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 694-710	If the list of processes @ROW and a physical is a member of (@ROW) and another physical is a member of (@ROW) and another entity element of (@ROW) is equal to the physical and a third entity element of (@ROW) is equal to the other physical and a positive integer is less than another positive integer, then the time of existence of the physical happens earlier than the time of existence of the other physical
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 771-781	If a list is the list of items viewed by an agent and a process is a member of the list, then the process is an instance of accessing web page and the agent is an agent of the process and there exists an entity such that the entity is an instance of web page and the process ends up at web page
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3113-3116	If an entity is a member of a list, then there exists a positive integer such that the positive integerth element of the list is equal to the entity

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 357-390	A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth 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 403-436	A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth 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 310-342	A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth 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 272-293	A real number is an average of a list if and only if there exist another list and a positive integer such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all another positive integer if the other positive integer is a member of the other list, then there exist another real number, the other real numberMINUSONE,, , a third positive integer and a fourth positive integer such that the other real number is greater than 1 and the other real number is less than or equal to length of the other list and the other positive integerth element of the other list is equal to the other real number and the third positive integer is a member of the list and the other real number is equal to the third positive integerth element of the list and the fourth positive integer is a member of the other list and the other real numberMINUSONE is equal to (the other real number and 1) and the other real numberMINUSONE is equal to the fourth positive integerth element of the other list and the other positive integer is equal to (the third positive integer and the fourth positive integer) and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer
No TPTP formula. May not be expressible in strict first order.	Music.kif 280-287	If a cognitive agent is a performer on an album, then there exist a content bearing object and a process such that the content bearing object is an instance of recording and the content bearing object is a member of the album and the content bearing object is a record of the process and the cognitive agent is an agent of the process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7596-7611	If amount a kind of substance, a corpuscular object and a real number an unit of mass(s) and a kind of substanceI is an instance of the kind of substance and the measure of the kind of substanceI is the real number2 the unit of mass(s) and the kind of substanceI is a part of the corpuscular object, then there exists a list such that the real number2 the unit of mass(s) is a member of the list and the list is equal to Amounts fn the kind of substance, the corpuscular object and the unit of mass and the real number is equal to the sum of the list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4861-4872	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the other integer mod the integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4874-4888	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer if the third integer is a member of (@ROW), then the third integer mod the other integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4946-4956	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the integer mod the other integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4958-4972	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is less than the integer and for all a third integer if the third integer is a member of (@ROW), then the other integer mod the third integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Music.kif 936-946	If a kind of data storage device is equal to the set of copies on a kind of data storage deviceS of an album and a third data storage device is an instance of the kind of data storage device, then for all an object if the object is a member of the album, then there exists a content bearing object such that the content bearing object is a copy of the object and the content bearing object is stored on the third data storage device
No TPTP formula. May not be expressible in strict first order.	Weather.kif 2005-2017	If a list is equal to Mean3SecondWindSpeedListFn ending at a time interval in region a geographic area and a function quantity is a member of the list, then there exist the time intervalLIST and another time interval such that the time intervalLIST is equal to ConsecutiveTimeIntervalList for at the time interval at 3 second duration(s) is contained in TimeIntervalListFn and the other time interval is a member of the time intervalLIST and the function quantity is equal to Mean3SecondWindSpeedFn for the other time interval in region the geographic area
No TPTP formula. May not be expressible in strict first order.	Media.kif 801-812	If an object is an instance of digital data storage device and a symbolic string is a part of the object and the symbolic string is an instance of digital data, then there exist a code map, a list and an entity such that the symbolic string in the code map denotes the entity and the list expresses the code map and if the entity is a member of the list, then the entity is an instance of binary number
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1532-1547	If a water wave is an instance of water wave and The waveHeight of the water wave a length measure., then there exist a list, a water area,, , an unit of measure and a real number such that the length measure is a member of the list and the water area is an instance of water area and the water wave is located at the water area and the unit of measure is an instance of unit of length and significantWaveHeight in the water area during the time of existence of the water wave is the real number the unit of measure(s). and the real number is equal to 4.0 and The StandardDeviationFn of the list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5369-5374	If a real number is an average of a list, then for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 464-468	If @ROW is the opposite of , then if another entity is a member of (@ROW), then the other entity is an instance of attribute
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2950-2955	If a class is disjointly decomposed into @ROW, then for all a third class if the third class is a member of (@ROW), then the third class is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2957-2966	If a class is disjointly decomposed into @ROW, then for all a third class and a fourth class if the third class is a member of (@ROW) and the fourth class is a member of (@ROW) and the third class is not equal to the fourth class, then the third class is disjoint from the fourth class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 574-578	If @ROW is disjointly decomposed into @ROW, then if another entity is a member of (@ROW), then the other entity is an instance of class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4854-4859	If the greatest common divisor of @ROW is equal to an integer, then if another entity is a member of (@ROW), then the other entity is an instance of number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4939-4944	If the least common multiple of @ROW is equal to an integer, then if another entity is a member of (@ROW), then the other entity is an instance of number
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1685-1692	If a real number is equal to The maximum value of the a list, then there doesn't exist another real number such that the other real number is a member of the list and the other real number is greater than the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 509-517	If @ROW are all the attributes of another kind of attribute, then for all an entity if the entity is an instance of another kind of attribute, then there exists another entity such that the other entity is a member of (@ROW) and the entity is equal to the other entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2940-2948	If a class is covered by @ROW, then for all an entity if the entity is an instance of the class, then there exists a third class such that the third class is a member of (@ROW) and the entity is an instance of the third class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 558-562	If @ROW is covered by @ROW, then if another entity is a member of (@ROW), then the other entity is an instance of class

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: