| 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 | Le nombre 1 argument de UnionFn est une instance de ensemble ou classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5431-5431 | Le nombre 2 argument de UnionFn est une instance de ensemble ou classe |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5428-5428 | UnionFn est une instance de fonction binaire |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5429-5429 | UnionFn est une instance de relation total |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5432-5432 | Le domaine de UnionFn est une instance de ensemble 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 secteur g�ographique and mesure de longueur le longueur de la classe d�crite par cha�ne sympbolique est mesure de longueur |
| 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 l' union de USMilitaryRankO3 et USMilitaryRankO4 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5509-5509 | Le nombre 1 argument de CardinalityFn est une instance de l' union de ensemble ou classe et collection |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2309-2310 | udaCanSignify l' union de PressingKeyFn TabKey et 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