| 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 20134-20134 | |
| 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 20133-20133 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20132-20132 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 119-119 | |
| 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 3006-3011 |
|
| 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 931-931 | 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 7578-7578 | 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 1777-1777 | The number 1 argument of attr is a subclass of object |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6234-6234 | The number 1 argument of BodyAreaFn is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15018-15018 | 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 1170-1170 | 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 1047-1047 | 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 30009-30009 | 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 8625-8625 | The number 2 argument of day is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18554-18554 | The number 1 argument of Dead fn is a subclass of organic object |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18318-18318 | 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 18582-18582 | 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 18653-18653 | 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 10197-10197 | 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 15554-15554 | 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 4514-4514 | 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 3667-3667 | 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 3724-3724 | 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 14904-14904 | 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 5499-5499 | 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 5488-5488 | 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. | Geography.kif 6913-6913 | The number 1 argument of geographic part type fn is a subclass of geographic area |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8650-8650 | The number 2 argument of hour is a subclass of day |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18297-18297 | The number 1 argument of impaired body part fn is a subclass of body part |
| 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