| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2249-2250 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4991-4993 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 913-914 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4987-4987 | 域 最大, 1 and Number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4988-4988 | 域 最大, 2 and Number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4983-4983 | 例 最大 and AssociativeFunction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4982-4982 | 例 最大 and BinaryFunction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4984-4984 | 例 最大 and CommutativeFunction |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4986-4986 | 例 最大 and TotalValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4989-4989 | 範圍 最大 and Number |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 710-710 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 712-712 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 428-428 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 175-175 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2145-2145 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 380-380 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 923-923 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 213-213 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 450-450 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 479-479 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 347-347 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36587-36587 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 711-711 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36586-36586 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36585-36585 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 348-348 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4995-5006 |
|
|
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