| 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 171-176 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 169-169 | The number 1 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 170-170 | The number 2 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 167-167 | subrelation is an instance of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 168-168 | 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 329-329 | |
| 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 55765-55765 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55764-55764 |
| 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 19683-19687 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 184-188 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 198-203 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 178-182 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 236-240 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 190-196 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 316-320 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 343-347 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2332-2334 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2459-2459 | Aborted launch is a subrelation of aborted |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2413-2413 | Aborted mission is a subrelation of aborted |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7014-7014 | Citizenry is a subrelation of resident |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6362-6362 | Density is a subrelation of per |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14932-14932 | DepartmentOfPreventingFn is a subrelation of department |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5958-5958 | Shoreline is a subrelation of border |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6374-6374 | Speed is a subrelation of per |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3133-3133 | abbreviatedDisplayTitle is a subrelation of displayTitle |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23449-23449 | 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 5816-5816 | abstractCounterpart is a subrelation of represents |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1622-1622 | abstraction level is a subrelation of property |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 228-228 | account at is a subrelation of party to agreement |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 247-247 | account holder is a subrelation of party to agreement |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4380-4380 | account information is a subrelation of contains information |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4126-4126 | accountPhoneNumber is a subrelation of account information |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4134-4134 | account used is a subrelation of patient |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3004-3004 | acronym is a subrelation of abbreviation |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 373-373 | administrative center is a subrelation of geopolitical subdivision |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3263-3263 | after tax income is a subrelation of income earned |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7185-7185 | age is a subrelation of measure |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2340-2340 | agent is a subrelation of involved in event |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3394-3394 | agentName is a subrelation of names |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2223-2223 | 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 21888-21888 | 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