| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1494-1495 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 363-366 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 55-56 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 60-62 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 361-361 | The number 1 argument of valence is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 362-362 | The number 2 argument of valence is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 359-359 | valence is an instance of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 360-360 | valence is an instance of single valued relation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 327-327 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 332-332 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 186-186 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 309-309 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2006-2006 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 138-138 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 181-181 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 431-431 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 60-60 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 206-206 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 196-196 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 61220-61220 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 328-328 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 61219-61219 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 61218-61218 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 180-184 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3049-3056 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 180-184 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3406-3408 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3469-3471 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3458-3460 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3366-3368 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3486-3488 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3508-3510 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3519-3521 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3497-3499 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3528-3532 |
|
|
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