| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1729-1730 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1839-1840 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 337-338 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1836-1836 | 少于 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1837-1837 | 少于 的 2 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1831-1831 | 少于 是 二元谓语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1833-1833 | 少于 是 非自反关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1834-1834 | 少于 是 延伸数量关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1832-1832 | 少于 是 传递关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1835-1835 | 少于 是 实数 的 trichotomizingOn |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 141-141 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 142-142 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 92-92 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 163-163 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1919-1919 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 44-44 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 76-76 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 172-172 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 202-202 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 111-111 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 91-91 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 325-325 | |
| 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. | chinese_format.kif 142-142 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34144-34144 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34143-34143 | |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 52-52 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 326-326 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 7524-7530 | 自身连接物体 是 液体滴 的 instance 和 1 的 approximate diameter 是 %2 和 500.0 是 lessThan 实数 若且唯若 那个 自身连接物体 是 小滴液体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3051-3062 | 有存在 金融工具， 那个 金融工具Price， and 和 另一个 实数 这样 协议 是 看涨期权 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 金融工具Price 是 lessThan 那个 另外 实数 若且唯若 那个 施事体 是 那个 协议 的 out 资兂短缺 |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3002-3013 | 有存在 金融工具， 那个 金融工具Price， and 和 另一个 实数 这样 协议 是 看涨期权 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 另外 实数 是 lessThan 那个 金融工具Price 若且唯若 那个 施事体 是 那个 协议 的 in 金钱 |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3015-3026 | 有存在 金融工具， 那个 金融工具Price， and 和 另一个 实数 这样 协议 是 放选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 金融工具Price 是 lessThan 那个 另外 实数 若且唯若 那个 施事体 是 那个 协议 的 in 金钱 |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3064-3075 | 有存在 金融工具， 那个 金融工具Price， and 和 另一个 实数 这样 协议 是 放选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 另外 实数 是 lessThan 那个 金融工具Price 若且唯若 那个 施事体 是 那个 协议 的 out 资兂短缺 |
| 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. | FinancialOntology.kif 783-788 | |
| 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. | FinancialOntology.kif 701-714 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 759-775 |
|
| 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. | Mid-level-ontology.kif 269-274 | |
| 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. | Merge.kif 13880-13893 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2667-2673 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13809-13818 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13820-13829 | |
| 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. | Catalog.kif 430-445 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5968-5982 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5950-5962 |
|
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3682-3695 |
|
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3708-3721 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1240-1246 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 238-264 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | 实数 是 负实数 的 instance 若且唯若 那个 实数 是 lessThan 0 和 那个 实数 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1867-1871 | 实数 是 lessThanOrEqualTo 另一个 实数 若且唯若 那个 实数 equal 那个 另外 实数 或 那个 实数 是 lessThan 那个 另外 实数 |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 172-187 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 155-170 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18728-18737 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18743-18753 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18759-18769 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18775-18785 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 1148-1156 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2623-2628 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13577-13586 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13505-13514 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13516-13527 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13467-13477 | |
| 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. | Mid-level-ontology.kif 4868-4872 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 772-795 |
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1391-1400 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1940-1954 |
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 892-898 | |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 882-890 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4698-4708 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10961-10974 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 620-630 | |
| 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. | Merge.kif 6099-6106 | 不存在 图路径 和 另一个 图路径 这样 那个 图路径 是 把 图 分成另外两个图的路径 Set 的 instance 和 那个 另外 图路径 是 把 那个 图 分成另外两个图的最短路径 Set 的 instance 和 那个 图路径 的 length 是 正整数 和 那个 另外 图路径 的 length 是 另一个 正整数 和 那个 正整数 是 lessThan 那个 另外 正整数 |
|
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