| 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 | The number 1 argument of union is an instance of set or class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5430-5430 | The number 2 argument of union is an instance of set or class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5427-5427 | Union is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5428-5428 | Union is an instance of total valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5431-5431 | The range of union is an instance of set or class |
| 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 60014-60014 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60013-60013 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 60012-60012 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 294-306 | A length measure is a length of unclassified gauge railway of a geographic area if and only if the length of the class described by a symbolic string is the length measure |
| 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 | The union of US military rank o3 and US military rank o4 is a command rank of echelon of company- military |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5508-5508 | The number 1 argument of cardinality is an instance of the union of set or class and collection |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2309-2310 | The union of pressing the tab key key and shift key hold down isgnifies selecting active area |
|
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