| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1987-1990 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3342-3348 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 620-624 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3340-3340 | 子類 Predicate and 可繼承的關係 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3339-3339 | 子類 Predicate and Relation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 455-455 | 例 相反的屬性 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 564-564 | 例 不相交分解 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 486-486 | 例 詳盡的屬性 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 546-546 | 例 徹底分解 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 580-580 | 例 劃分 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 686-686 | 例 進程列表 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2162-2162 | 劃分 Relation, Predicate and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3478-3478 | 子類 BinaryPredicate and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18470-18470 | 子類 ClosedWorldPredicate and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3550-3550 | 子類 邏輯運算符 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3500-3500 | 子類 QuaternaryPredicate and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3511-3511 | 子類 QuintaryPredicate and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3489-3489 | 子類 TernaryPredicate and Predicate |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 915-915 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1037-1037 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 591-591 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 121-121 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 124-124 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2276-2276 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 543-543 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 126-126 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 158-158 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 612-612 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 125-125 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18440-18440 | 域 defaultMaxValue, 1 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18423-18423 | 域 defaultMinValue, 1 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18457-18457 | 域 defaultValue, 1 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18405-18405 | 域 maxValue, 1 and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18387-18387 | 域 minValue, 1 and Predicate |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2998-3003 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3005-3010 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2106-2113 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2093-2103 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2075-2090 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2137-2150 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 447-453 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3610-3618 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2210-2223 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2174-2187 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 192-198 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3048-3055 |
|
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