| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1987-1990 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3343-3349 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 620-624 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3341-3341 | 谓语 是 可继承的关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3340-3340 | 谓语 是 关系 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 455-455 | 相反属性 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 564-564 | 不相交的分拆 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 486-486 | 详尽的属性 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 546-546 | 彻底的分拆 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 580-580 | 划分 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 686-686 | 进程列表 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2162-2162 | 关系 详尽无遗地 partition 成 谓语 和 函数 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3479-3479 | 二元谓语 是 谓语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18549-18549 | ClosedWorldPredicate 是 谓语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3551-3551 | 逻辑运算符 是 谓语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3501-3501 | 四元谓语 是 谓语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3512-3512 | 五元谓语 是 谓语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3490-3490 | 三元谓语 是 谓语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 915-915 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1037-1037 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 591-591 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 121-121 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 124-124 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2276-2276 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 543-543 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 126-126 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 158-158 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 612-612 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 125-125 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18519-18519 | defaultMaxValue 的 1 数量 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18502-18502 | defaultMinValue 的 1 数量 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18536-18536 | defaultValue 的 1 数量 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18484-18484 | maxValue 的 1 数量 是 谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18466-18466 | minValue 的 1 数量 是 谓语 的 instance |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2999-3004 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3006-3011 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2106-2113 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2093-2103 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2075-2090 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2137-2150 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 447-453 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3611-3619 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2210-2223 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2174-2187 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 192-198 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3049-3056 |
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
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