| 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 133-135 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 27-29 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 28-30 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | 子类别 的 1 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | 子类别 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | 子类别 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18442-18442 | 子类别 是 ClosedWorldPredicate 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | 子类别 是 偏序关系 的 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 324-324 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 182-182 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 271-271 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2002-2002 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 134-134 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 175-175 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 419-419 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 308-308 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 202-202 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 192-192 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 463-463 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21288-21288 | 子领域 是 子类别 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5391-5391 | 子集 是 子类别 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55716-55716 | |
| 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 55715-55715 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55714-55714 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3984-4004 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1186-1201 |
|
| No TPTP formula. May not be expressible in strict first order. | Biography.kif 730-740 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 789-793 |
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 976-980 | |
| 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. | Government.kif 619-625 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 504-520 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 522-538 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13519-13530 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13488-13499 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 957-961 | |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 963-967 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2112-2121 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2156-2165 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2202-2211 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1980-1989 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2876-2882 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4629-4634 |
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4693-4699 | |
| 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 18350-18355 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4945-4950 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4166-4172 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4532-4543 |
|
| 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. | Mid-level-ontology.kif 31304-31311 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1478-1491 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24185-24195 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 221-227 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3005-3010 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 244-250 | |
| 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. | Economy.kif 4945-4950 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4532-4543 |
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5258-5265 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5032-5036 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5235-5244 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1780-1788 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3840-3845 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3963-3968 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3993-3998 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11984-11996 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3904-3909 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3934-3939 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3872-3877 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3948-3953 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5485-5493 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18033-18041 | |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3447-3476 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 219-223 |
|
| 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. | Military.kif 895-906 | 地缘政治区域 的 fit 对于军服务男性 equal 符号串 所描述的类别 instance 的数量 |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5109-5112 | 有存在 有点 客体 这样 有点 客体 是 HandToolBox 的 subclass 和 manufacturer 那个 有点 客体 and SortimoCorp |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1170-1170 | AAM 是 空袭导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1169-1169 | AAM 是 空中发射导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1171-1171 | AAM 是 导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1647-1647 | AAV 是 两栖车辆 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1646-1646 | AAV 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1648-1648 | AAV 是 乘用车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1649-1649 | AAV 是 动力车辆 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Muscles.kif 778-778 | ABranchOfDorsalPrimaryDivisionOfSuboccipitalNerve 是 Nerve 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26287-26287 | ACPowerSource 是 能量源 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3293-3293 | ADHD 是 心理功能障碍 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1123-1123 | AG m 是 空中发射导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1124-1124 | AG m 是 地面攻击导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1203-1203 | AG m114 是 AG m 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1205-1205 | AG m114 是 反装甲武器 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1204-1204 | AG m114 是 束骑导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1136-1136 | AG m65 是 AG m 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1138-1138 | AG m65 是 反装甲武器 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1137-1137 | AG m65 是 红外导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1889-1889 | A h1 是 直升机 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1890-1890 | A h1 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1177-1177 | AI m9 是 AAM 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1178-1178 | AI m9 是 红外导弹 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25478-25478 | AMFMAlarmClock 是 AlarmClock 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25479-25479 | AMFMAlarmClock 是 无线电接收器 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 293-293 | AM广播电台 是 广播电台 的 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