TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1970-1972
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3076-3079
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 602-604
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3072-3072	The number 1 argument of list concatenate is an instance of list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3073-3073	The number 2 argument of list concatenate is an instance of list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3070-3070	List concatenate is an instance of binary function
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3071-3071	List concatenate is an instance of total valued relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3074-3074	The range of list concatenate is an instance of list

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 267-267
No TPTP formula. May not be expressible in strict first order.	english_format.kif 272-272
No TPTP formula. May not be expressible in strict first order.	french_format.kif 152-152
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 166-166
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1980-1980
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 104-104
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 344-344
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 205-205
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 171-171
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 158-158
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 331-331
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34667-34667
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 268-268
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34666-34666
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34665-34665
No TPTP formula. May not be expressible in strict first order.	terms-de.txt 110-110
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 332-332

antecedent

No TPTP formula. May not be expressible in strict first order.

Merge.kif 3083-3102

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

consequent

No TPTP formula. May not be expressible in strict first order.

Merge.kif 3190-3202

If a list is equal to the sub-list from a positive integer to an integer of another list and (the integer and the positive integer) is greater than 1,
then the list is equal to the list composed of (the positive integerth element of the other list) and the sub-list from (1 and the positive integer) to the integer of the other list

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

KB Term:			Term intersection

English Word: