TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1492-1493
No TPTP formula. May not be expressible in strict first order.	Merge.kif 336-337
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 53-54
No TPTP formula. May not be expressible in strict first order.	spanish_format.kif 58-59
No TPTP formula. May not be expressible in strict first order.	Merge.kif 334-334	子类别的范围的 1 数量是函数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 335-335	子类别的范围的 2 数量是类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 333-333	子类别的范围是非对称关系的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 332-332	子类别的范围是二元谓语的 instance

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 329-329
No TPTP formula. May not be expressible in strict first order.	english_format.kif 334-334
No TPTP formula. May not be expressible in strict first order.	french_format.kif 187-187
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 240-240
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2007-2007
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 139-139
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 433-433
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 278-278
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 207-207
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 198-198
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 432-432
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 330-330
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 48764-48764
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 48763-48763
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 48762-48762

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 339-343	如果函数的所得值是有点类的 subclass 和那个函数(@ROW) equal 另一个类，然后那个另外类是有点类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 351-357	如果函数的所得值是有点类的 subclass 和那个函数的所得值是另一个有点类的 subclass，然后有点类是另一个有点类的 subclass 或那个另外有点类是那个有点类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 440-445	如果函数的所得值是有点类的 subclass 和另一个函数的所得值是另一个有点类的 subclass 和有点类和 % 2 是 disjoint，然后那个函数和那个另外函数是 disjoint 关系
No TPTP formula. May not be expressible in strict first order.	Merge.kif 345-349	如果函数是另一个函数的 subrelation 和那个另外函数的所得值是有点类的 subclass，然后那个函数的所得值是有点类的 subclass

consequent

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

Merge.kif 345-349

如果函数是另一个函数的 subrelation 和那个另外函数的所得值是有点类的 subclass，
然后那个函数的所得值是有点类的 subclass

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	WMD.kif 88-88	AgentOfOrganismFn 的所得值是生物制剂的 subclass
No TPTP formula. May not be expressible in strict first order.	Music.kif 932-932	AlbumCopiesFn 的所得值是 DataStorageDevice 的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1776-1776	Attr 的所得值是客体的 subclass
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 6235-6235	BodyAreaFn 的所得值是身体部位的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 14973-14973	BodySideFn 的所得值是身体部位的 subclass
No TPTP formula. May not be expressible in strict first order.	Government.kif 675-675	宪法的所得值是宪法的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 29726-29726	CoveringFn 的所得值是可穿戴物品的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6072-6072	分图路径函数的所得值是图路径的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8590-8590	日函数的所得值是日的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 116-116	DeadFn 的所得值是 OrganismRemains 的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30631-30631	DemonymFn 的所得值是 NationalPerson 的 subclass
No TPTP formula. May not be expressible in strict first order.	Geography.kif 3013-3013	文献的所得值是文本的 subclass
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 9980-9980	EdemaFn 的所得值是 Edema 的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15510-15510	版本函数的所得值是有内用物体的 subclass
No TPTP formula. May not be expressible in strict first order.	Government.kif 1686-1686	选举的所得值是选举的 subclass
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4515-4515	FailureFn 的所得值是过程的 subclass
No TPTP formula. May not be expressible in strict first order.	Food.kif 3668-3668	FarmOfProductFn 的所得值是耕地面积的 subclass
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3698-3698	财政年度的所得值是时距的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 14859-14859	FoodForFn 的所得值是自身连接物体的 subclass
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6915-6915	GeographicPartTypeFn 的所得值是地理区域的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6056-6056	图路函数的所得值是图路径的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8615-8615	时函数的所得值是小时的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13470-13470	ImpairmentFn 的所得值是生物过程的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6585-6585	间隔函数的所得值是恒量的 subclass
No TPTP formula. May not be expressible in strict first order.	Food.kif 2600-2600	JuiceOfFn 的所得值是 Juice 的 subclass

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: