| 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 5434-5436 | |
| 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 5430-5430 | O argumento numero 1 de UnionFn e' uma instancia de Conjunto ou Classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5431-5431 | O argumento numero 2 de UnionFn e' uma instancia de Conjunto ou Classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5428-5428 | UnionFn e' uma instancia de Funcao Binaria |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5429-5429 | UnionFn e' uma instancia de Relacao Total |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5432-5432 | O contra-dominio de UnionFn e' uma instancia de Conjunto ou Classe |
| 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 60004-60004 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60003-60003 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60002-60002 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 294-306 | lengthOfUnclassifiedGaugeRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento |
| 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 | commandRankOfEchelon CompanyMilitary and a uniao de USMilitaryRankO3 e USMilitaryRankO4 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5509-5509 | O argumento numero 1 de CardinalityFn e' uma instancia de a uniao de Conjunto ou Classe e Colecao |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2309-2310 | udaCanSignify a uniao de PressingKeyFn TabKey e ShiftKeyHoldDown and 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