| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1731-1732 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1852-1854 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 339-340 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1848-1848 | 大于 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1849-1849 | 大于 的 2 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1842-1842 | 大于 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1845-1845 | 大于 是 非自反关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1846-1846 | 大于 是 延伸数量关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1843-1843 | 大于 是 总值关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1844-1844 | 大于 是 传递关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1850-1850 | 大于 是 少于 的 inverse |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1847-1847 | 大于 是 实数 的 trichotomizingOn |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4676-4676 | 南部海洋 comparative 地区 大于 对于 2.0 跟 美国 在一起 |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 111-111 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 111-111 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 77-77 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 121-121 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1904-1904 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 29-29 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 77-77 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 127-127 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 161-161 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 96-96 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 76-76 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 248-248 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 112-112 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 26532-26532 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 26531-26531 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 26530-26530 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 37-37 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 249-249 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1007-1011 | 实体 是 个人账户 的 instance 和 符号串 所描述的类别 instance 的数量 是 greaterThan 1 若且唯若 那个 实体 是 联名账户 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 7440-7451 | 客体 是 悬浮颗粒 的 instance 和 自身连接物体 是 那个 客体 的 part 和 1 的 approximate diameter 是 %2 和 10.0 是 greaterThan 实数 和 那个 实数 是 greaterThan 2.5 若且唯若 有存在 那个 客体10 这样 那个 客体10 是 粗悬浮颗粒 的 instance 和 那个 客体10 是 那个 客体 的 part |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 367-385 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1370-1377 | |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 809-825 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15515-15532 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3277-3284 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3258-3268 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3068-3089 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3190-3202 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1453-1465 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1070-1075 | |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2884-2902 |
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1017-1023 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1575-1582 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 354-365 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8722-8729 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8731-8736 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 342-348 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2942-2947 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1753-1773 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13863-13878 |
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1398-1405 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5997-6017 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13798-13807 | |
| 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. | Geography.kif 4711-4720 | 公海 是 客体 的 attribute 若且唯若 有存在 物理 和 实数 这样 那个 客体 是 盐水区 的 instance 和 那个 客体 不 是 内陆水域 的 instance 和 那个 物理 和 那个 客体 的 distance 是 那个 实数 海里 和 那个 实数 是 greaterThan 5.0 |
| 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. | Merge.kif 1885-1889 | 实数 是 greaterThanOrEqualTo 另一个 实数 若且唯若 那个 实数 equal 那个 另外 实数 或 那个 实数 是 greaterThan 那个 另外 实数 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1937-1941 | 实数 是 正实数 的 instance 若且唯若 那个 实数 是 greaterThan 0 和 那个 实数 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7758-7766 | 客体 larger 另一个 客体 若且唯若 对所有 实数， 另一个 实数， and 和 测量单位 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1754-1759 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1766-1771 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 1165-1176 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 204-223 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3984-4004 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1186-1201 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1538-1544 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1522-1530 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1597-1603 | |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 809-825 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18446-18451 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13536-13545 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13547-13558 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13486-13497 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13566-13575 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 18429-18434 | |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2585-2603 |
|
| 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. | Mid-level-ontology.kif 18343-18358 | |
| 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