| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2838-2840 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9680-9683 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1582-1584 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9677-9677 | 表面 的 1 数量 是 自身连接物体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9678-9678 | 表面 的 2 数量 是 自身连接物体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9674-9674 | 表面 是 非对称关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9675-9675 | 表面 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9676-9676 | 表面 是 表面部分 的 subrelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 373-373 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 374-374 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 215-215 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 290-290 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2021-2021 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 167-167 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 222-222 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 498-498 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 61-61 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 235-235 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 232-232 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 482-482 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 374-374 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 56286-56286 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 56285-56285 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1462-1467 | 飞机 的 altitude 是 自身连接物体 和 那个 自身连接物体 是 行星地球 的 surface 和 那个 飞机 是 飞机 的 instance 若且唯若 高度测量 是 absolute 那个 飞机 的高度 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2693-2704 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2665-2676 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17736-17741 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17764-17769 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 7142-7162 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 7497-7509 |
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1488-1496 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4819-4833 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1316-1322 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1324-1329 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1331-1336 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4837-4842 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4830-4835 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3999-4010 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9685-9690 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 2781-2786 | 客体 是 长度测量 above 地表 若且唯若 有存在 自身连接物体 这样 那个 客体 的 altitude 是 那个 自身连接物体 和 那个 自身连接物体 是 行星地球 的 surface |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 7497-7509 |
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1441-1451 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3188-3196 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21147-21177 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5003-5008 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8848-8857 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9396-9402 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1205-1210 |
|
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2302-2308 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3262-3273 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10991-10998 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 473-480 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3472-3481 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 328-333 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3991-3997 |
|
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