| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2158-2161 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4431-4435 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 815-819 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4428-4428 | 域 名, 1 and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4429-4429 | 域 名, 2 and Entity |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4427-4427 | 例 名 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4426-4426 | 子關係 名 and 參照 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 309-309 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 314-314 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 177-177 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1997-1997 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 129-129 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 197-197 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3424-3424 | 子關係 agentName and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23214-23214 | 子關係 別號 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27217-27217 | 子關係 傳統的長名 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27228-27228 | 子關係 傳統的短名稱 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14725-14725 | 子關係 姓 and 名 |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2205-2205 | 子關係 filename and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14718-14718 | 子關係 以前的名字 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3290-3290 | 子關係 fullName and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14742-14742 | 子關係 給予的名稱 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14757-14757 | 子關係 當地的長名 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14762-14762 | 子關係 本地簡稱 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14738-14738 | 子關係 中間名字 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3337-3337 | 子關係 nameIndexOrder and 名 |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2095-2095 | 子關係 密碼 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14705-14705 | 子關係 標題 and 名 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4437-4437 | 子關係 獨特標識符 and 名 |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2058-2058 | 子關係 userName and 名 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 39669-39669 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3406-3411 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3374-3380 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3339-3344 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3429-3433 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3446-3450 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3480-3484 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13257-13262 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24632-24643 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24645-24655 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24584-24586 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3218-3226 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 31-33 |
|
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2506-2509 | 持有期間 未來 TimePosition and 名 "Republic of Serbia" and Serbia 例 TimePosition and 天 5 and 月 June and 年 2006 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2533-2536 | 持有期間 未來 TimePosition and 例 TimePosition and 天 3 and 月 June and 年 2006 名 "Montenegro" and Montenegro |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2495-2495 | 名 "Adana" and 阿達納土耳其 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2497-2497 | 名 "Addis Ababa" and 亞的斯亞貝巴埃塞俄比亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2499-2499 | 名 "Aden" and 腺也門 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2501-2501 | 名 "Adora" and 阿多拉西岸 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 352-352 | 名 "Advanced Developing Country" and 發達的先進國家 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4160-4160 | 名 "Afghanistan" and 阿富汗 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3522-3522 | 名 "Africa" and 非洲 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2503-2503 | 名 "Afula" and 阿富拉以色列 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2505-2505 | 名 "Agri" and 阿格里土耳其 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2507-2507 | 名 "Ain Defla" and ain defla 阿爾及利亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2509-2509 | 名 "Ain el Hajar" and ain el hajar 阿爾及利亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2511-2511 | 名 "Ajaccio" and ajaccio 法國 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2513-2513 | 名 "Al-Balamand " and al balamand 黎巴嫩 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4064-4064 | 名 "Albania" and 阿爾巴尼亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2515-2515 | 名 "Alei Sinai" and alei sinai 加沙地帶 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2517-2517 | 名 "Alei Zahav" and alei zahav 西方銀行 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2519-2519 | 名 "Aley" and 阿萊黎巴嫩 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 3946-3946 | 名 "Algeria" and 阿爾及利亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2521-2521 | 名 "Algiers" and 阿爾及爾，阿爾及利亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2523-2523 | 名 "Alkhan-Yurt" and 烷烴蒙古包俄羅斯 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2525-2525 | 名 "Alon Moreh" and alon |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2527-2527 | 名 "Ambon" and 安汶印度尼西亞 |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 813-813 | 名 "American Football" and 美式足球赛 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 4194-4194 | 名 "American Samoa" and 美國薩摩亞 |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 2529-2529 | 名 "Amman" and 安曼，約旦 |
| 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