| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1496-1498 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 366-370 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 57-60 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 63-67 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 362-362 | The number 1 argument of documentation is an instance of entity |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 363-363 | The number 2 argument of documentation is an instance of human language |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 364-364 | The number 3 argument of documentation is an instance of symbolic string |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 361-361 | documentation is an instance of ternary predicate |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 97-97 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 97-97 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 71-71 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 81-81 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1897-1897 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 23-23 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 110-110 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 121-121 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 90-90 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 70-70 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 115-115 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20067-20067 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 98-98 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20066-20066 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20065-20065 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 31-31 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 178-178 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2538-2538 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3222-3223 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4419-4421 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28255-28256 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3295-3308 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27210-27211 | |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 295-296 | |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 237-239 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 4076-4078 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2917-2919 | |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5380-5389 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3267-3268 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3602-3606 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3678-3678 | |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4877-4878 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2140-2146 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2132-2138 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2123-2130 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2148-2154 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2162-2163 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2159-2160 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2156-2158 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2165-2167 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6440-6442 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6480-6485 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|
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