| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1387-1389 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 233-236 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 45-47 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 49-52 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 230-230 | The number 1 argument of domain subclass is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 231-231 | The number 2 argument of domain subclass is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-232 | The number 3 argument of domain subclass is an instance of class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 229-229 | domain subclass 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 293-293 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 298-298 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 169-169 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 84-84 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1989-1989 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 121-121 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 178-178 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 381-381 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 124-124 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 189-189 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 176-176 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 118-118 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20115-20115 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 294-294 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20114-20114 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20113-20113 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 184-184 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2992-2997 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 244-250 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 426-431 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 238-242 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 238-242 |
|
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 87-87 | The number 1 argument of Agent of organism fn is a subclass of organism |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 930-930 | The number 2 argument of album copies function is a subclass of data storage device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7563-7563 | The number 1 argument of Amounts fn is a subclass of substance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1764-1764 | The number 1 argument of attr is a subclass of object |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14862-14862 | The number 2 argument of Body side fn is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 656-656 | The number 2 argument of cell part is a subclass of cell part |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1046-1046 | The number 1 argument of contest function is a subclass of contest |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29830-29830 | The number 1 argument of Covering fn is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8573-8573 | The number 2 argument of day is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 115-115 | The number 1 argument of Dead fn is a subclass of OrganicObjecct |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18120-18120 | The number 1 argument of dead or missing body part fn is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18164-18164 | The number 2 argument of department is a subclass of physical |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18228-18228 | The number 2 argument of Department of preventing fn is a subclass of process |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9931-9931 | The number 1 argument of edema is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15392-15392 | The number 1 argument of edition is a subclass of content bearing object |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4512-4512 | The number 1 argument of failure fn is a subclass of intentional process |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1081-1081 | The number 1 argument of farm of product fn is a subclass of organism |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3740-3740 | The number 2 argument of fiscal year starting is a subclass of year |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14748-14748 | The number 1 argument of food for fn is a subclass of organism |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5484-5484 | The number 1 argument of generalized intersection is a subclass of set or class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5473-5473 | The number 1 argument of generalized union is a subclass of set or class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8598-8598 | The number 2 argument of hour is a subclass of day |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18099-18099 | The number 1 argument of impaired body part fn is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13360-13360 | The number 1 argument of impairment is a subclass of physiologic process |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 577-577 | The number 1 argument of juice of fn is a subclass of fruit or vegetable |
| 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