| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3693-3694 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16554-16556 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16552-16552 | 域 父親, 1 and Organism |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16553-16553 | 域 父親, 2 and Organism |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16546-16546 | 例 父親 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16545-16545 | 例 父親 and PartialValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16544-16544 | 例 父親 and SingleValuedRelation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 527-527 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 532-532 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 311-311 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 109-109 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2079-2079 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 263-263 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 317-317 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 686-686 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 149-149 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 332-332 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 341-341 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 228-228 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 528-528 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23375-23375 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23374-23374 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 208-208 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 229-229 |
| antecedent |
|
|
| 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. | Merge.kif 16558-16560 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24710-24725 | Human Human 是 cousins 女人 人 Human 的 grandmother 是 女人 Human 的 grandfather 是 人 Human 的 grandmother 是 女人 Human 的 grandfather 是 人 Organism Organism 母親 Human and Organism 父親 Human and Organism 母親 Human and Organism 父親 Human and Organism |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24801-24808 | 人 是 Human 的 stepfather Human 母親 Human and Human 人 是 Human 的 spouse 父親 Human and 人 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24818-24825 | 女人 是 Human 的 stepfather Human 父親 Human and Human 女人 是 Human 的 spouse 母親 Human and 女人 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10431-10438 | |
| 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 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. | ArabicCulture.kif 686-692 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 672-678 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 616-622 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 742-748 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 644-650 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 728-734 | |
| 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. | ArabicCulture.kif 792-798 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21788-21795 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 590-595 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 564-569 |
|
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