| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1973-1975 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3109-3111 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 605-607 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3106-3106 | 在列表内 的 1 数量 是 实体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3107-3107 | 在列表内 的 2 数量 是 串列 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3104-3104 | 在列表内 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3105-3105 | 在列表内 是 部分值关系 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 131-131 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 132-132 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 87-87 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 147-147 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1914-1914 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 39-39 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 103-103 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 157-157 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 186-186 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 106-106 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 86-86 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 298-298 | |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 332-332 | albumTrack 是 在列表内 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30193-30193 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 132-132 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30192-30192 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30191-30191 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 47-47 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 299-299 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3286-3290 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2005-2017 |
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1998-2003 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 503-507 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 497-501 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7582-7587 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1975-1980 |
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1966-1973 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2491-2498 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2483-2489 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1929-1933 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1716-1720 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1784-1788 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1750-1754 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1819-1823 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2677-2682 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1769-1775 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1860-1864 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16921-16929 | |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 694-710 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 771-781 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3113-3116 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 357-390 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 403-436 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 310-342 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | 实数 是 串列 的 average 若且唯若 有存在 另一个 串列 和 正整数 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数
|
| No TPTP formula. May not be expressible in strict first order. | Music.kif 280-287 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7596-7611 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4861-4872 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4874-4888 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4946-4956 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4958-4972 | |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 936-946 |
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2005-2017 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 801-812 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1532-1547 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 464-468 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2950-2955 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2957-2966 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 574-578 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4854-4859 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4939-4944 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1685-1692 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 509-517 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2940-2948 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 558-562 | |
| 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