| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1216-1219 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1213-1213 | 区域总设施类型 的 1 数量 是 地理区域 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1214-1214 | 区域总设施类型 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1215-1215 | 区域总设施类型 的 3 数量 是 非负整数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1212-1212 | 区域总设施类型 是 三元谓语 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2491-2491 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2490-2490 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2489-2489 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 58550-58550 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 58549-58549 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 58548-58548 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1277-1287 | 地理区域 是 对于 非负整数 在地区 和 机场有着铺设跑道 对应的 Class 的 total 设施类别 若且唯若 有存在 符号串 和 实体 这样 那个 非负整数 是 那个 符号串 所描述的类别 的 cardinality |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1221-1228 | 地理区域 是 对于 非负整数 在地区 类 的 total 设施类别 若且唯若 那个 非负整数 是 符号串 所描述的类别 的 cardinality |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1482-1491 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1237-1245 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1289-1296 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1230-1235 |
|
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