| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1371-1373 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-134 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | 子类别 的 1 数量 是 集或类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | 子类别 的 2 数量 是 集或类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 128-128 | 子类别 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | 子类别 是 偏序关系 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 319-319 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 327-327 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5107-5107 | 子集 是 子类别 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55618-55618 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55617-55617 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55616-55616 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1140-1152 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1853-1857 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 784-788 |
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 931-935 | |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 48-56 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2859-2865 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 606-612 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 480-496 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 498-514 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11172-11183 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11143-11154 |
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 912-916 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 918-922 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2116-2125 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2160-2169 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2206-2215 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1984-1993 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 195-200 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16089-16093 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16095-16104 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2281-2290 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 334-349 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 351-365 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 784-805 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 289-308 |
|
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 793-795 | 集或类 是 类 的 instance 若且唯若 那个 集或类 是 实体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 219-225 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2894-2899 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 242-248 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 195-200 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 215-219 |
|
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 204-208 |
|
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 178-182 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 225-229 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11909-11913 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14486-14490 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3269-3273 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28220-28249 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 322-328 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 337-341 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 349-355 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18742-18749 | |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 74-78 | |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14683-14687 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1206-1208 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1233-1235 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2839-2844 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6259-6261 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1684-1693 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3171-3173 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5090-5093 | 有存在 施事体 这样 那个 施事体 是 HandToolBox 的 subclass 和 manufacturer SortimoCorp and 那个 施事体 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1300-1300 | 球孢子菌 posadasii 的 biological agent 是 危及生命的特工 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1293-1293 | 球孢子菌丝虫 的 biological agent 是 危及生命的特工 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1479-1479 | 疟疾疟原虫 的 biological agent 是 生物制剂 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1288-1288 | Serratia marcenscens 的 biological agent 是 危及生命的特工 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1840-1840 | 蜱传脑炎病毒 的 biological agent 是 危及生命的特工 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 400-400 | 鼠疫耶尔森氏菌 的 biological agent 是 危及生命的特工 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3938-3938 | 一个 dead 苹果 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3964-3964 | 一个 dead 鳄梨 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3967-3967 | 一个 dead 香蕉 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3935-3935 | 一个 dead 浆果 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3970-3970 | 一个 dead 面包果 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3843-3843 | 一个 dead 卷心菜 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3876-3876 | 一个 dead 胡萝卜 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3896-3896 | 一个 dead 木薯 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3846-3846 | 一个 dead 菜花 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3944-3944 | 一个 dead 柑橘类水果 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3973-3973 | 一个 dead 椰子 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3840-3840 | 一个 dead 黄瓜 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3976-3976 | 一个 dead 日期水果 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4019-4019 | 一个 dead 食用坚果 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3849-3849 | 一个 dead 茄子 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3927-3927 | 一个 dead 葡萄 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4033-4033 | 一个 dead 花生 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3837-3837 | 一个 dead 绿叶蔬菜 是 杂货生产 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3979-3979 | 一个 dead 芒果 是 杂货生产 的 subclass |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|
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