| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1443-1447 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14114-14119 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14112-14112 | 地缘政治分区 的 1 数量 是 地缘政治区域 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14113-14113 | 地缘政治分区 的 2 数量 是 地缘政治区域 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14109-14109 | 地缘政治分区 是 非对称关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14110-14110 | 地缘政治分区 是 传递关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14111-14111 | 地缘政治分区 是 地理分区域 的 subrelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 804-804 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 814-814 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 483-483 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 815-815 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 435-435 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 505-505 | |
| 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. | Government.kif 403-403 | 主要地缘政治细分 是 地缘政治分区 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 805-805 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 25842-25842 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 25841-25841 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 25840-25840 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 4668-4673 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 4535-4540 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 482-485 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 395-397 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8079-8084 | 地缘政治区域 是 市区 的 instance 若且唯若 有存在 另一个 地缘政治区域 这样 那个 另外 地缘政治区域 是 城市 的 instance 和 那个 地缘政治区域 是 那个 另外 地缘政治区域 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2432-2445 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6931-6936 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 477-480 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19691-19699 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4255-4255 | Beijing 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4275-4275 | Chengdu 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4259-4259 | Chongqing 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4267-4267 | Guangzhou 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4279-4279 | Nanjing 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4251-4251 | Shanghai 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4271-4271 | Shenzhen 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4263-4263 | Tianjin 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4283-4283 | Wuhan 是 中国 的地缘政治部分 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4287-4287 | 西安 是 中国 的地缘政治部分 |
|
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