| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2291-2293 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5433-5435 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 960-962 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5429-5429 | 域 聯盟, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5430-5430 | 域 聯盟, 2 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5427-5427 | 例 聯盟 and BinaryFunction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5428-5428 | 例 聯盟 and TotalValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5431-5431 | 範圍 聯盟 and SetOrClass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 494-494 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 499-499 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 290-290 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 306-306 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2067-2067 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 242-242 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 641-641 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 342-342 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 311-311 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 318-318 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 498-498 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 495-495 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60002-60002 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60001-60001 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60000-60000 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 294-306 | LengthMeasure 是 GeographicArea 的未分類規格軌道 length length 卡帕 SymbolicString and 位於 SymbolicString and GeographicArea 例 SymbolicString and 聯盟 標準軌距鐵路 and 聯盟 寬軌鐵路 and 聯盟 DualGaugeRailway and 窄軌鐵路 and LengthMeasure |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 558-570 | |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 179-188 |
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Military.kif 742-743 | 聯盟 美國軍銜o3 and 美國軍銜o4 是 公司- 軍事 的 command 梯隊等級 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5508-5508 | 域 基數, 1 and 聯盟 SetOrClass and Collection |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2309-2310 | 聯盟 pressing TabKey 鍵 and ShiftKeyHoldDown isgnifies SelectingActiveArea |
|
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