| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1500-1501 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 390-392 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 63-64 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 72-74 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 388-388 | 域 不相交的, 1 and Class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 389-389 | 域 不相交的, 2 and Class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 386-386 | 例 不相交的 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 387-387 | 例 不相交的 and SymmetricRelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 285-285 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 290-290 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 165-165 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 75-75 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1985-1985 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 117-117 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 109-109 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 182-182 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 370-370 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 59-59 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 185-185 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 172-172 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 166-166 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 562-562 | 相關的內部概念 不相交分解 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 407-407 | 相關的內部概念 不相交的關係 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 286-286 | 相關的內部概念 不相交的關係 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19863-19863 | 相關的內部概念 不相交的關係 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19862-19862 | 相關的內部概念 不相交的關係 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19861-19861 | 相關的內部概念 不相交的關係 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 115-115 | 相關的內部概念 不相交的關係 and 不相交的 |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 167-167 | 相關的內部概念 不相交的關係 and 不相交的 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 412-417 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 419-424 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 426-431 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 433-438 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 394-400 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2963-2968 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2952-2961 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 974-974 | 不相交的 在線以上 and 在線下面 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8862-8862 | 不相交的 下午 and Evening |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 360-360 | 不相交的 AltKey and ControlKey |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 362-362 | 不相交的 AltKey and FunctionKey |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 361-361 | 不相交的 AltKey and ShiftKey |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1313-1313 | 不相交的 AltKeyHoldDown and ControlKeyHoldDown |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1312-1312 | 不相交的 AltKeyHoldDown and ShiftKeyHoldDown |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9422-9422 | 不相交的 無氧運動裝置 and 有氧運動裝置 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20685-20685 | 不相交的 午前 and 發布meridiem |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8124-8124 | 不相交的 公寓樓 and 單身家庭住所 |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 295-295 | 不相交的 ArrowKey and EnterKey |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16059-16059 | 不相交的 Article and Book |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 172-172 | 不相交的 火砲 and 軍用坦克 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 6345-6345 | 不相交的 瀝青 and 化石燃料 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14127-14127 | 不相交的 AstronomicalBody and GeographicArea |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12453-12453 | 不相交的 Attaching and Detaching |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1656-1656 | 不相交的 AudioInput and JoystickMotion |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1657-1657 | 不相交的 AudioInput and KeyboardAction |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1655-1655 | 不相交的 AudioInput and TouchSurfaceAction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10259-10259 | 不相交的 自主過程 and IntentionalProcess |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17118-17118 | 不相交的 穀倉 and 住宅樓 |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 752-752 | 不相交的 棒球偷 and 棒球擊中 |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 751-751 | 不相交的 棒球偷 and 棒球步行 |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 760-760 | 不相交的 棒球罷工 and 棒球擊中 |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 708-708 | 不相交的 棒球步行 and 棒球擊中 |
| 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