| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1375-1378 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 167-172 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 33-37 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 35-39 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 165-165 | The number 1 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 166-166 | The number 2 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 163-163 | subrelation is an instance of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 164-164 | subrelation is an instance of partial ordering relation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 321-321 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 326-326 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 183-183 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 279-279 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2003-2003 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 135-135 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 176-176 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 422-422 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 316-316 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 203-203 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 193-193 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 471-471 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 322-322 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55820-55820 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55819-55819 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 134-134 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 119-121 | A relation is a subrelation of involved in event if and only if the relation is an instance of case role |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 43-52 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24906-24910 |
|
| 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 194-199 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 174-178 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-236 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 186-192 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 312-316 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 338-342 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2423-2425 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2513-2513 | Aborted launch is a subrelation of aborted |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2434-2434 | Aborted mission is a subrelation of aborted |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9223-9223 | Citizenry is a subrelation of resident |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6652-6652 | Density is a subrelation of per |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19977-19977 | Department of preventing fn is a subrelation of department |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6246-6246 | Shoreline is a subrelation of border |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6664-6664 | Speed is a subrelation of per |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3147-3147 | abbreviated display title is a subrelation of display title |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28893-28893 | abbreviation is a subrelation of conventional short name |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 868-868 | absorbed dose is a subrelation of measure |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6123-6123 | abstract counterpart is a subrelation of represents |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1743-1743 | abstraction level is a subrelation of property |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 230-230 | account at is a subrelation of party to agreement |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 249-249 | account holder is a subrelation of party to agreement |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4404-4404 | account information is a subrelation of contains information |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4150-4150 | account phone number is a subrelation of account information |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4158-4158 | account used is a subrelation of patient |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28904-28904 | acronym is a subrelation of abbreviation |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 385-385 | administrative center is a subrelation of geopolitical subdivision |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3340-3340 | after tax income is a subrelation of income earned |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7546-7546 | age is a subrelation of measure |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2431-2431 | agent is a subrelation of involved in event |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3408-3408 | agent name is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2198-2198 | agent operates in area is a subrelation of partly located |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27332-27332 | air temperature is a subrelation of measure |
| 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