TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1375-1378
No TPTP formula. May not be expressible in strict first order.	Merge.kif 173-178
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 33-37
No TPTP formula. May not be expressible in strict first order.	spanish_format.kif 35-39
No TPTP formula. May not be expressible in strict first order.	Merge.kif 171-171	子关系的 1 数量是关系的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 172-172	子关系的 2 数量是关系的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 169-169	子关系是二元谓语的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 170-170	子关系是偏序关系的 instance

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 321-321
No TPTP formula. May not be expressible in strict first order.	english_format.kif 326-326
No TPTP formula. May not be expressible in strict first order.	french_format.kif 183-183
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 279-279
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2003-2003
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 135-135
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 176-176
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 422-422
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 316-316
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 203-203
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 193-193
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 471-471
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 322-322
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55787-55787
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55786-55786

antecedent

No TPTP formula. May not be expressible in strict first order.	Media.kif 119-121	关系是参与活动的 subrelation 若且唯若那个关系是格角色的 instance
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 43-52	如果属性是属性的 instance 和另一个属性是属性的 instance 和二元谓语是属于的 subrelation，然后 ~{ 那个属性和那个另外属性是对于那个二元谓语的 mutually exclusive } 或 ~{ 那个二元谓语实体 and 那个属性 } 或 ~{ 那个二元谓语那个实体 and 那个另外属性 }
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23246-23250	如果客体对于过程在事件格角色 plays 角色和那个格角色是那个格角色2 的 subrelation，然后那个客体对于那个过程在事件那个格角色2 plays 角色
No TPTP formula. May not be expressible in strict first order.	Merge.kif 186-190	如果关系是另一个关系的 subrelation 和那个另外关系的正整数数量是类的 instance，然后那个关系的那个正整数数量是那个类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 200-205	如果关系是另一个关系的 subrelation 和那个另外关系是类的 instance 和那个类是可继承的关系的 subclass，然后那个关系是那个类的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 180-184	如果关系是另一个关系的 subrelation 和那个关系 % 有正整数 Argument，然后那个另外关系 % 有那个正整数 Argument
No TPTP formula. May not be expressible in strict first order.	Merge.kif 238-242	如果关系是另一个关系的 subrelation 和那个另外关系的正整数数量是类的 subclass，然后那个关系的那个正整数数量是那个类的 subclass
No TPTP formula. May not be expressible in strict first order.	Merge.kif 192-198	如果关系是另一个关系的 subrelation 和那个关系是谓语的 instance 和那个另外关系是谓语的 instance 和那个关系 @ROW，然后那个另外关系 @ROW
No TPTP formula. May not be expressible in strict first order.	Merge.kif 318-322	如果函数是另一个函数的 subrelation 和那个另外函数的 range 是类的实例，然后那个函数的 range 是那个类的实例
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 2427-2429

如果关系是格角色的 instance，
然后那个关系是参与活动的 subrelation

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 2479-2479	中止发射是中止的 subrelation
No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 2433-2433	任务中止是中止的 subrelation
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 8037-8037	公民是居民的 subrelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6642-6642	密度函数是每的 subrelation
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18389-18389	DepartmentOfPreventingFn 是 DepartmentOfFn 的 subrelation
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6176-6176	海岸线是边界的 subrelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6654-6654	速率函数是每的 subrelation
No TPTP formula. May not be expressible in strict first order.	Media.kif 3163-3163	abbreviatedDisplayTitle 是 displayTitle 的 subrelation
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 27233-27233	缩写是传统的短名称的 subrelation
No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 868-868	吸收剂量是计量的 subrelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6113-6113	abstractCounterpart 是表示的 subrelation
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1617-1617	抽象层次是特性的 subrelation
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 228-228	帐号在是协议的一方的 subrelation
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 247-247	帐户持有人是协议的一方的 subrelation
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4409-4409	accountInformation 是包含信息的 subrelation
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4155-4155	accountPhoneNumber 是 accountInformation 的 subrelation
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 4163-4163	accountUsed 是受事的 subrelation
No TPTP formula. May not be expressible in strict first order.	Media.kif 3034-3034	acronym 是缩写的 subrelation
No TPTP formula. May not be expressible in strict first order.	Government.kif 385-385	行政中心是地缘政治分区的 subrelation
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3323-3323	税后收入是赚的收入的 subrelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7517-7517	年龄是计量的 subrelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2435-2435	主事是参与活动的 subrelation
No TPTP formula. May not be expressible in strict first order.	Media.kif 3424-3424	agentName 是命名的 subrelation
No TPTP formula. May not be expressible in strict first order.	Government.kif 2237-2237	代理人在区域内经营是有一部分位于的 subrelation
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 25675-25675	气温是计量的 subrelation

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: