| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1492-1493 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 329-330 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 53-54 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 58-59 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 327-327 | 域 範圍子類, 1 and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 328-328 | 域子類 範圍子類, 2 and Class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 326-326 | 例 範圍子類 and BinaryPredicate |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 329-329 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 334-334 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 187-187 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 240-240 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2007-2007 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 139-139 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 433-433 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 278-278 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 207-207 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 198-198 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 432-432 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 330-330 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48797-48797 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48796-48796 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48795-48795 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 138-138 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 332-336 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 344-350 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 433-438 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 338-342 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 338-342 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 88-88 | 範圍子類 AgentOfOrganismFn and 生物製劑 |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 932-932 | 範圍子類 AlbumCopiesFn and DataStorageDevice |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1769-1769 | 範圍子類 attr and Object |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6216-6216 | 範圍子類 BodyAreaFn and BodyPart |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15077-15077 | 範圍子類 BodySideFn and BodyPart |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 639-639 | 範圍子類 憲法 and 憲法 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31391-31391 | 範圍子類 CoveringFn and 可穿戴物品 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6063-6063 | 範圍子類 切集 and GraphPath |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8660-8660 | 範圍子類 天 and Day |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18610-18610 | 範圍子類 DeadFn and OrganismRemains |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32311-32311 | 範圍子類 DemonymFn and NationalPerson |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3001-3001 | 範圍子類 文獻 and Text |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11329-11329 | 範圍子類 EdemaFn and Edema |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15611-15611 | 範圍子類 版 and ContentBearingObject |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1648-1648 | 範圍子類 選舉 and 選舉 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4515-4515 | 範圍子類 FailureFn and Process |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3668-3668 | 範圍子類 FarmOfProductFn and 耕地面積 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4033-4033 | 範圍子類 財政年度 and TimeInterval |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14963-14963 | 範圍子類 FoodForFn and SelfConnectedObject |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6984-6984 | 範圍子類 GeographicPartTypeFn and GeographicArea |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6047-6047 | 範圍子類 圖形路徑 and GraphPath |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8685-8685 | 範圍子類 小時 and Hour |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13575-13575 | 範圍子類 ImpairmentFn and BiologicalProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6576-6576 | 範圍子類 間隔 and ConstantQuantity |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2600-2600 | 範圍子類 JuiceOfFn and Juice |
| 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