TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1748-1748
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1969-1969
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 356-356
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1967-1967	Integer is exhaustively partitioned into negative integer and nonnegative integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1966-1966	Integer is exhaustively partitioned into odd integer and even integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1965-1965	Integer is a subclass of rational number

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	Military.kif 934-934	The range of available for military service male is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5534-5534	The range of cardinality is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4812-4812	The range of ceiling is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 6789-6789	The range of demand is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4839-4839	The range of denominator is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Military.kif 956-956	The range of fit for military service male is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4857-4857	The range of floor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4875-4875	The range of greatest common divisor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4960-4960	The range of least common multiple is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5065-5065	The range of numerator is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 33639-33639	The range of population is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5363-5363	The range of predecessor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Military.kif 994-994	The range of reaching military age annually male is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5126-5126	The range of remainder is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5218-5218	The range of signum is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5330-5330	The range of successor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 6760-6760	The range of supply is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1971-1971	Even integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1996-1996	Negative integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1986-1986	Nonnegative integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1976-1976	Odd integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1981-1981	Prime number is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 866-866	Prime number is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	english_format.kif 934-934	Prime number is a subclass of integer

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

appearance as argument number 3

No TPTP formula. May not be expressible in strict first order.	Merge.kif 4848-4848	The number 2 argument of exponentiation is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4876-4876	The number 1 argument of greatest common divisor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4961-4961	The number 1 argument of least common multiple is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5362-5362	The number 1 argument of predecessor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5124-5124	The number 1 argument of remainder is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5125-5125	The number 2 argument of remainder is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3174-3174	The number 1 argument of sub-list function is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3175-3175	The number 2 argument of sub-list function is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5329-5329	The number 1 argument of successor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8668-8668	The number 1 argument of year is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Weather.kif 3779-3779	The number 2 argument of air quality index is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11710-11710	The number 3 argument of breathing rate is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 792-792	The number 3 argument of capacity by arrangement is an instance of integer
No TPTP formula. May not be expressible in strict first order.	VirusProteinAndCellPart.kif 705-705	The number 2 argument of chromosome number is an instance of integer
No TPTP formula. May not be expressible in strict first order.	VirusProteinAndCellPart.kif 831-831	The number 3 argument of chromosome set count is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3173-3173	The number 2 argument of coil count is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Communications.kif 135-135	The number 3 argument of communication satellite for area is an instance of integer
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 753-753	The number 2 argument of criticality level is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18628-18628	The number 2 argument of default max value is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18611-18611	The number 2 argument of default min value is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18645-18645	The number 2 argument of default value is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Media.kif 2072-2072	The number 2 argument of exact cardinality is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Media.kif 2073-2073	The number 3 argument of exact cardinality is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 3965-3965	The number 2 argument of Fleet Size is an instance of integer
No TPTP formula. May not be expressible in strict first order.	engineering.kif 837-837	The number 2 argument of gear tooth count is an instance of integer

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 5114-5119	If a real number is an instance of integer and equal the real number and 0, then equal 1 and the real number and the reciprocal of the real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 32892-32907	If there is a shortage of a quantity of a kind of object for a cognitive agent at a currency measure during a time interval and the quantity is an instance of integer, then the cognitive agent desires there exist an entity and another entity such that the entity is an instance of buying and the time of existence of the entity takes place during the time interval and the object transferred in the entity is the other entity and the currency measure is a transaction amount of the entity and the cognitive agent is an agent of the entity and the other entity is an instance of collection and a kind of object is a member type of the other entity and the quantity is a member count of the other entity and the cognitive agent possesses the other entity
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 32834-32844	If there is a shortage of a quantity of a kind of object for a cognitive agent at a currency measure during a time interval and the quantity is an instance of integer, then the cognitive agent desires there exists an entity such that the entity is an instance of collection and a kind of object is a member type of the entity and the quantity is a member count of the entity and the cognitive agent possesses the entity
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 32859-32874	If there is a shortage of an integer of a kind of object for an agent at a currency measure during a time interval and the integer is an instance of integer, then there don't exist a transfer and a collection such that the transfer is an instance of buying and the time of existence of the transfer takes place during the time interval and the object transferred in the transfer is the collection and the currency measure is a transaction amount of the transfer and the agent is an agent of the transfer and the collection is an instance of collection and a kind of object is a member type of the collection and the integer is a member count of the collection and the agent possesses the collection
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5356-5358	If an integer is an instance of integer, then equal the integer and ((the integer+1)+2)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5352-5354	If an integer is an instance of integer, then equal the integer and ((the integer+2)+1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5372-5374	If an integer is an instance of integer, then the integer is greater than (the integer+2)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5339-5341	If an integer is an instance of integer, then the integer is less than (the integer+1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5110-5112	If a real number is an instance of integer, then equal the reciprocal of the real number and the real number raised to the power -1

consequent

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 25883-25893	If a day is a birthdate of a human and the day is an instance of the day a positive integer of month the month a kind of month, then there exist another kind of day and an integer such that the human's birthday is another kind of day and the other kind of day is a subclass of day and the integer is an instance of integer and equal the other kind of day and the day the positive integer of month the month a kind of month and the integer is greater than another integer
No TPTP formula. May not be expressible in strict first order.	Biography.kif 71-87	If a process is an instance of bar mitzvah and a human is a patient of the process and the human is an instance of boy and the human is a member of a collection and the collection is an instance of judaism and a day is a birthdate of the human and the day is an instance of the day a positive integer of month the month a kind of month, then there exist an integer and a time position such that the integer is an instance of integer and equal the integer and (another integer and 13) and the time position is an instance of the day the positive integer of month the month a kind of month and equal the time of existence of the process and immediately after the time position
No TPTP formula. May not be expressible in strict first order.	Biography.kif 102-118	If a process is an instance of bat mitzvah and a human is a patient of the process and the human is an instance of girl and the human is a member of a collection and the collection is an instance of judaism and a day is a birthdate of the human and the day is an instance of the day a positive integer of month the month a kind of month, then there exist an integer and a time position such that the integer is an instance of integer and equal the integer and (another integer and 13) and the time position is an instance of the day the positive integer of month the month a kind of month and equal the time of existence of the process and immediately after the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3407-3411	If a function is an instance of sequence function and the range of the function is an instance of a class, then the class is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 25842-25853	If a physical is an instance of wedding and date of the physical is a day and the day is an instance of the day a positive integer of month the month a kind of month, then there exist another kind of day and an integer such that wedding anniversary the physical and another kind of day and the other kind of day is a subclass of day and the integer is an instance of integer and equal the other kind of day and the day the positive integer of month the month a kind of month and the integer is greater than another integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4927-4932	If an integer is a multiplicative factor of another integer, then there exists a real number such that the real number is an instance of integer and equal the integer and the other integer and the real number

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

Show without tree

Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners

KB Term:			Term intersection

English Word: