|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9013-9013 | successorClass 的 1 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9014-9014 | successorClass 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4531-4531 | total 的 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. | Merge.kif 3660-3660 | 含全序关系 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3682-3682 | 含三分律关系 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 335-335 | 子类别的范围 的 2 数量 是 类 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2129-2129 | 集或类 详尽无遗地 partition 成 集合 和 类 |
|
|
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