| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1492-1493 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 329-330 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 53-54 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 58-59 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 327-327 | The number 1 argument of range subclass is an instance of function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 328-328 | The number 2 argument of range subclass is a subclass of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 326-326 | range subclass is an instance of binary predicate |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 329-329 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 334-334 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 187-187 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 240-240 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2007-2007 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 139-139 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 433-433 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 278-278 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 207-207 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 198-198 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 432-432 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 330-330 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48768-48768 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48767-48767 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48766-48766 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 138-138 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 332-336 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 344-350 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 433-438 |
|
| 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 338-342 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 88-88 | The values returned by Agent of organism fn are subclasses of biological agent |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 934-934 | The values returned by album copies function are subclasses of data storage device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1786-1786 | The values returned by attr are subclasses of object |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6252-6252 | The values returned by body area are subclasses of body part |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15126-15126 | The values returned by Body side fn are subclasses of body part |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 639-639 | The values returned by constitution are subclasses of constitution |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31645-31645 | The values returned by Covering fn are subclasses of wearable item |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6097-6097 | The values returned by cut set are subclasses of graph path |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8703-8703 | The values returned by day are subclasses of day |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18664-18664 | The values returned by Dead fn are subclasses of organism remains |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32565-32565 | The values returned by Demonym fn are subclasses of national person |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3171-3171 | The values returned by document are subclasses of text |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11309-11309 | The values returned by edema are subclasses of swelling |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15660-15660 | The values returned by edition are subclasses of content bearing object |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1648-1648 | The values returned by election are subclasses of election |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4510-4510 | The values returned by failure fn are subclasses of process |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3675-3675 | The values returned by farm of product fn are subclasses of cultivated land area |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4035-4035 | The values returned by fiscal year are subclasses of time interval |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15012-15012 | The values returned by food for fn are subclasses of self connected object |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 7252-7252 | The values returned by geographic part type fn are subclasses of geographic area |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6081-6081 | The values returned by graph path are subclasses of graph path |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8728-8728 | The values returned by hour are subclasses of hour |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13624-13624 | The values returned by impairment are subclasses of biological process |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6610-6610 | The values returned by interval are subclasses of constant quantity |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2607-2607 | The values returned by juice of fn are subclasses of juice |
| 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