| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1633-1634 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1277-1279 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 216-217 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 256-258 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1272-1272 | 域 會員, 1 and Physical |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1273-1273 | 域 會員, 2 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1269-1269 | 例 會員 and AsymmetricRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1270-1270 | 例 會員 and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1271-1271 | 例 會員 and IntransitiveRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1275-1275 | 相關的內部概念 會員 and 元件 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1274-1274 | 相關的內部概念 會員 and 例 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 153-153 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 154-154 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 97-97 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 182-182 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1925-1925 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 49-49 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 69-69 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 185-185 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 220-220 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 116-116 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 96-96 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 358-358 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2388-2388 | 子關係 在組織中關聯 and 會員 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8743-8743 | 子關係 小組成員 and 會員 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18188-18188 | 子關係 student and 會員 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18260-18260 | 子關係 teacher and 會員 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37015-37015 | 子關係 teacher and 會員 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 154-154 | 子關係 teacher and 會員 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37014-37014 | 子關係 teacher and 會員 |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37013-37013 | 子關係 teacher and 會員 |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 57-57 | 子關係 teacher and 會員 |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 359-359 | 子關係 teacher and 會員 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3565-3567 | 會員 Physical and 國際紅十字和紅新月運動 會員 Physical and 國際紅十字會和紅新月會聯合會 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 506-510 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2579-2583 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2659-2663 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3231-3235 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3276-3280 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4043-4047 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3534-3543 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3528-3532 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3545-3555 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3582-3591 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3576-3580 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3593-3603 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2735-2745 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3189-3194 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8751-8758 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1729-1734 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 972-976 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3185-3189 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25143-25153 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3202-3215 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3239-3259 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23997-24005 | |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 108-122 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 145-160 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 676-678 | attribute Object and 信仰團體 的 member 會員 Object and 信仰團體 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 702-704 | attribute Object and 不可知 會員 Object and 不可知論 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1347-1349 | attribute Object and ahmadiyya穆斯林 會員 Object and ahmadiyya教派 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1225-1227 | attribute Object and 英國國教 會員 Object and 英國國教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1233-1235 | attribute Object and 英國國教 會員 Object and 英格蘭教堂 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 720-722 | attribute Object and 無神論者 會員 Object and 無神論 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 757-759 | attribute Object and 巴哈 會員 Object and 巴哈主義 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 769-771 | attribute Object and 佛教徒 會員 Object and 佛教 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 925-927 | attribute Object and Capitalist 會員 Object and Capitalism |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 895-897 | attribute Object and Communism 會員 Object and Communism |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1306-1308 | attribute Object and 儒 會員 Object and 儒 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1361-1363 | attribute Object and 德魯茲穆斯林 會員 Object and 德魯茲教派 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1247-1249 | attribute Object and 東正教基督教 會員 Object and 東正教基督教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1318-1320 | attribute Object and 印度教 會員 Object and 印度教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1411-1413 | attribute Object and 耆那教 會員 Object and 耆那教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1330-1332 | attribute Object and 穆斯林 會員 Object and 伊斯蘭教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1457-1459 | attribute Object and neopaganismist 會員 Object and neopaganism |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1261-1263 | attribute Object and 新教 會員 Object and 新教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1428-1430 | attribute Object and 宗教的猶太人 會員 Object and 猶太教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1283-1285 | attribute Object and 羅馬天主教徒 會員 Object and 羅馬天主教會 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1275-1277 | attribute Object and 羅馬天主教徒 會員 Object and 羅馬天主教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1377-1379 | attribute Object and 什葉派穆斯林 會員 Object and 什葉派 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1472-1474 | attribute Object and 神道教 會員 Object and 神道 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1487-1489 | attribute Object and 錫克教 會員 Object and 錫克教 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1396-1398 | attribute Object and 遜尼派穆斯林 會員 Object and 遜尼派 |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | TimeInterval 例 TimeInterval and TimeInterval 飾面 TimeInterval and 何時 JesusOfNazareth 啟動 TimeInterval and 何時 TwelveApostles entity
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3181-3181 | 會員 丹麥 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3182-3182 | 會員 瑞典 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3183-3183 | 會員 英國 and 歐洲貨幣聯盟 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3161-3161 | 會員 奧地利 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2618-2618 | 會員 貝克島 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2865-2865 | 會員 比利時 and 比荷盧經濟聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3162-3162 | 會員 比利時 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3163-3163 | 會員 塞浦路斯 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3164-3164 | 會員 愛沙尼亞 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3165-3165 | 會員 芬蘭 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3166-3166 | 會員 法國 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3167-3167 | 會員 德國 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3168-3168 | 會員 希臘 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2619-2619 | 會員 Howland島 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3169-3169 | 會員 愛爾蘭 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3170-3170 | 會員 意大利 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2620-2620 | 會員 賈維斯島 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2625-2625 | 會員 約翰斯頓環礁 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2621-2621 | 會員 金曼礁 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3171-3171 | 會員 拉脫維亞 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3172-3172 | 會員 立陶宛 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2867-2867 | 會員 盧森堡 and 比荷盧經濟聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3173-3173 | 會員 盧森堡 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3174-3174 | 會員 馬耳他 and 歐洲貨幣聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2626-2626 | 會員 中途島嶼 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2622-2622 | 會員 納瓦薩島 and UnitedStatesMinorOutlyingIslands |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2866-2866 | 會員 荷蘭 and 比荷盧經濟聯盟 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 3175-3175 | 會員 荷蘭 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