| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2823-2824 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9506-9507 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1565-1566 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9503-9503 | 相连 的 1 数量 是 客体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9504-9504 | 相连 的 2 数量 是 客体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9499-9499 | 相连 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9501-9501 | 相连 是 自反关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9500-9500 | 相连 是 空间关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9502-9502 | 相连 是 对称关系 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4200-4200 | 横过 和 相连 是 disjoint 关系 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 361-361 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 364-364 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 209-209 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 52-52 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2016-2016 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 161-161 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 86-86 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 216-216 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 480-480 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 93-93 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 229-229 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 226-226 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 120-120 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9570-9570 | 接触 和 相连 是 内部相关 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16095-16095 | 相连工程子组件 是 相连 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4033-4033 | 重叠 是 相连 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 362-362 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16638-16638 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16637-16637 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 16636-16636 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 121-121 | |
| 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 9715-9720 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9554-9560 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 514-518 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9521-9525 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12383-12397 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10577-10593 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5330-5335 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12431-12440 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17882-17892 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5380-5395 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10046-10050 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9745-9751 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9730-9735 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9509-9513 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17103-17107 | 客体 在 另一个 客体 的 邻 若且唯若 那个 客体 在 那个 另外 客体 的 近 或 那个 客体 和 那个 另外 客体 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 514-518 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11967-11977 |
|
| No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 32-46 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12360-12367 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12408-12415 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 690-700 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10647-10657 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10607-10617 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9515-9519 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2949-2957 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5661-5670 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11485-11492 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3538-3547 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10046-10050 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2698-2714 |
|
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 383-396 |
|
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 403-416 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10039-10044 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9546-9552 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24327-24334 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5442-5444 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9935-9937 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15366-15371 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5129-5136 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5169-5169 | 腺嘌呤 和 阿拉伯海 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5177-5177 | GulfOfMexico 和 加勒比海 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5176-5176 | GulfOfMexico 和 北大西洋 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5161-5161 | 阿曼湾 和 阿拉伯海 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4631-4631 | 印度洋 和 波斯湾 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4630-4630 | 印度洋 和 南太平洋 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4632-4632 | 印度洋 和 南部海洋 是 connected |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 744-744 | 密西西比河 和 GulfOfMexico 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5154-5154 | 波斯湾 和 霍尔木兹海峡 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5168-5168 | 红海 和 腺嘌呤 是 connected |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5160-5160 | 霍尔木兹海峡 和 阿曼湾 是 connected |
|
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