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 1997-1997
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 1994-1994	Positive integer is a subclass of nonnegative integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1995-1995	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 81-81
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 8624-8624	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 15555-15555	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 2979-2979	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 4977-4977	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 14690-14690	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 9004-9004	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 8702-8702	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 14645-14645	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 8986-8986	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 3440-3440	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 2243-2243	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 13819-13819	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 3457-3457	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 21736-21736	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 2324-2324	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 2503-2503	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 2491-2491	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 6694-6694	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 2620-2620	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 2696-2696	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 2684-2684	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 1588-1588	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 3084-3103	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 799-817	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 1999-2001	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: