TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1754-1754
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1984-1984
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 363-363
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1981-1981	Positive integer is a subclass of nonnegative integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1982-1982	Positive integer is a subclass of positive real number

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 872-872
No TPTP formula. May not be expressible in strict first order.	english_format.kif 946-946
No TPTP formula. May not be expressible in strict first order.	french_format.kif 548-548
No TPTP formula. May not be expressible in strict first order.	terms-hindi.txt 78-78
No TPTP formula. May not be expressible in strict first order.	terms-it.txt 79-79
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2233-2233
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 500-500
No TPTP formula. May not be expressible in strict first order.	terms-cb.txt 83-83
No TPTP formula. May not be expressible in strict first order.	terms-cz.txt 115-115
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 569-569
No TPTP formula. May not be expressible in strict first order.	terms-tg.txt 82-82

appearance as argument number 3

No TPTP formula. May not be expressible in strict first order.	Merge.kif 8572-8572	The number 1 argument of day is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15393-15393	The number 2 argument of edition is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2965-2965	The number 2 argument of list order is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4962-4962	The number 2 argument of log is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14533-14533	The number 2 argument of periodical issue is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8952-8952	The number 1 argument of quarter fn is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8650-8650	The number 1 argument of second is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14488-14488	The number 2 argument of series volume is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8934-8934	The number 1 argument of week fn is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3453-3453	The number 2 argument of account number is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2259-2259	The number 3 argument of agricultural product type by rank is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13664-13664	The number 2 argument of atomic number is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3470-3470	The number 2 argument of check number is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1209-1209	The number 2 argument of data stream slack is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 209-209	The number 2 argument of domain is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 231-231	The number 2 argument of domain subclass is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 21789-21789	The number 2 argument of electron number is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2340-2340	The number 3 argument of export commodity type by rank is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2519-2519	The number 3 argument of export partner by rank is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2507-2507	The number 3 argument of export partner by rank in period is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6667-6667	The number 2 argument of human capacity is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2636-2636	The number 3 argument of import commodity type by rank is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2712-2712	The number 3 argument of import partner by rank is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2700-2700	The number 3 argument of import partner by rank in period is an instance of positive integer
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1604-1604	The number 3 argument of industry rank by output is an instance of positive 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 3070-3089	If a list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list and a positive integer is less than or equal to length of the other list and another positive integer is less than or equal to length of the third list and the positive integer is an instance of positive integer and the other positive integer is an instance of positive integer, then the positive integerth element of the list is equal to the positive integerth element of the other list and (length of the other list and the other positive integer)th element of the list is equal to the other positive integerth element of the third list
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 989-1007	If a list is the list of items viewed by an agent and a process is an instance of accessing web page and another process is an instance of accessing web page and the agent is an agent of the process and the agent is an agent of the other process and a positive integer is an instance of positive integer and another positive integer is an instance of positive integer and the positive integerth element of the list is equal to the process and the other positive integerth element of the list is equal to the other process and the positive integer is greater than the other positive integer, then the time of existence of the other process happens earlier than the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1986-1988	If a real number is an instance of positive integer, then the real number is greater than 0

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: