| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3689-3690 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16493-16495 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16491-16491 | 域 親, 1 and Organism |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16492-16492 | 域 親, 2 and Organism |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16488-16488 | 例 親 and AsymmetricRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16486-16486 | 例 親 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16489-16489 | 例 親 and IntransitiveRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16490-16490 | 例 親 and TotalValuedRelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 523-523 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 528-528 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 309-309 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 209-209 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2077-2077 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 261-261 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 315-315 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 680-680 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 247-247 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 330-330 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 337-337 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 400-400 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16563-16563 | 子關係 女兒 and 親 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16574-16574 | 子關係 兒子 and 親 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44461-44461 | 子關係 兒子 and 親 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 524-524 | 子關係 兒子 and 親 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44460-44460 | 子關係 兒子 and 親 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 44459-44459 | 子關係 兒子 and 親 |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 206-206 | 子關係 兒子 and 親 |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 401-401 | 子關係 兒子 and 親 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10458-10464 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16619-16623 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16613-16617 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24676-24680 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24682-24686 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24670-24674 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16512-16520 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1890-1900 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16505-16510 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24835-24851 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16597-16605 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16607-16611 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16497-16499 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16501-16503 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 406-408 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24695-24700 | 女人 是 Human 的 aunt Human 女人 是 Human 的 sister 親 Human and Human |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24786-24791 | Human 的 uncle 是 人 Human 人 是 Human 的 brother 親 Human and Human |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10411-10416 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16607-16611 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16417-16425 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16427-16434 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16548-16550 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24732-24737 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24744-24749 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16522-16525 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1872-1881 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16531-16533 |
|
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