| 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 227-230 | |
| 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 224-224 | 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 225-225 | 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 226-226 | 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 223-223 | 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 20127-20127 | |
| 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 20126-20126 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20125-20125 | |
| 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 3003-3008 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 238-244 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 419-424 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-236 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-236 |
|
| 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 933-933 | 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 7612-7612 | 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 1772-1772 | The number 1 argument of attr is a subclass of object |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6251-6251 | The number 1 argument of body area is a subclass of body part |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15110-15110 | 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 1177-1177 | 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 1049-1049 | 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 31646-31646 | 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 8687-8687 | The number 2 argument of day is a subclass of month |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18648-18648 | 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 18411-18411 | 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 19895-19895 | 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 19966-19966 | 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 11308-11308 | 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 15643-15643 | 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 4509-4509 | 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 3674-3674 | 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 4061-4061 | 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 14996-14996 | 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 5508-5508 | 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 5497-5497 | 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 7079-7079 | 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 8712-8712 | The number 2 argument of hour is a subclass of day |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18390-18390 | 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