| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2434-2436 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6352-6356 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1125-1128 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6348-6348 | 计量函数 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6349-6349 | 计量函数 的 2 数量 是 测量单位 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6346-6346 | 计量函数 是 二元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6347-6347 | 计量函数 是 总值关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6350-6350 | 计量函数 的 range 是 物理量 的实例 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 633-633 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 636-636 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 383-383 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 178-178 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2113-2113 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 335-335 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 392-392 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 829-829 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 216-216 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 405-405 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 426-426 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36671-36671 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 634-634 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36670-36670 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36669-36669 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 353-353 |
| 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. | 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. | Geography.kif 7469-7479 | 客体 是 悬浮颗粒 的 instance 和 自身连接物体 是 那个 客体 的 part 和 1 的 approximate diameter 是 %2 和 实数 是 greaterThanOrEqualTo 2.5 若且唯若 有存在 那个 客体25 这样 那个 客体25 是 细悬浮颗粒 的 instance 和 那个 客体25 是 那个 客体 的 part |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3731-3733 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 北 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3755-3757 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 东南 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3739-3741 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 南 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3759-3761 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 西南 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3743-3745 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 西方 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3763-3765 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 西北 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3747-3749 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 北 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3751-3753 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 东北 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3735-3737 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 东 |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1702-1708 | 函数量 equal 实数 英里每小時 若且唯若 那个 函数量 equal 那个 实数 英里 除以 1 小时 |
| 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 1783-1787 | hearingAcuity 人类, -10 Decibel and 15 Decibel 若且唯若 NormalHearingSensitivity 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1794-1798 | hearingAcuity 人类, 16 Decibel and 25 Decibel 若且唯若 BorderlineHearingSensitivity 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1805-1809 | hearingAcuity 人类, 26 Decibel and 40 Decibel 若且唯若 MildHearingLoss 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1815-1819 | hearingAcuity 人类, 41 Decibel and 55 Decibel 若且唯若 ModerateHearingLoss 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1826-1830 | hearingAcuity 人类, 56 Decibel and 70 Decibel 若且唯若 ModeratelySevereHearingLoss 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1837-1841 | hearingAcuity 人类, 71 Decibel and 90 Decibel 若且唯若 SevereHearingLoss 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1848-1852 | hearingAcuity 人类, 91 Decibel and 200 Decibel 若且唯若 ProfoundHearingLoss 是 那个 人类 的 attribute |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13605-13611 | 物理 的 measure 是 实数 公吨 若且唯若 那个 物理 的 measure 是 那个 实数 和 2205.0 磅质量 |
| 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. | Weather.kif 2680-2690 | 实体 是 地区 的 instance 和 那个 实体 有 标准状况 的 attribute 在 时间位置 holdsDuring 若且唯若 298.15 凯文度 是 那个 实体 的 air 温度 和 29.530 英寸汞 是 那个 实体 的 barometric 压力 在 那个 时间位置 holdsDuring |
| 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 238-264 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
| 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. | Geography.kif 4711-4720 | 公海 是 客体 的 attribute 若且唯若 有存在 物理 和 实数 这样 那个 客体 是 盐水区 的 instance 和 那个 客体 不 是 内陆水域 的 instance 和 那个 物理 和 那个 客体 的 distance 是 那个 实数 海里 和 那个 实数 是 greaterThan 5.0 |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1928-1933 | compressionRatio 发动机 and 实数 若且唯若 minCylinderVolume 那个 发动机 and 另一个 实数 测量单位 和 maxCylinderVolume 那个 发动机 and 那个 测量单位AX 那个 测量单位 和 那个 实数 equal 那个 另外 实数 和 那个 测量单位AX |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1702-1708 | 函数量 equal 实数 英里每小時 若且唯若 那个 函数量 equal 那个 实数 英里 除以 1 小时 |
| 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. | Mid-level-ontology.kif 13605-13611 | 物理 的 measure 是 实数 公吨 若且唯若 那个 物理 的 measure 是 那个 实数 和 2205.0 磅质量 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 378-380 | 物理 的 measure 是 实数 圆周角度 若且唯若 那个 物理 的 measure 是 60.0 和 那个 实数 弧分 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 397-399 | 物理 的 measure 是 实数 弧分 若且唯若 那个 物理 的 measure 是 60.0 和 那个 实数 弧秒 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13326-13331 | 物理 的 measure 是 实数 OunceMass 若且唯若 那个 物理 的 measure 是 那个 实数 和 16.0 磅质量 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1129-1137 | 地缘政治区域 是 实数 测量单位 和 有点 时距 在 周期 行业属性 的 sector GDP 价值 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 地缘政治区域 是 对于 那个 实数 那个 测量单位 的 sector GDP 价值 那个 行业属性 在 那个 时间位置 holdsDuring |
| 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. | Geography.kif 2080-2090 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 2092-2106 |
|
| 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. | 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. | Hotel.kif 1186-1201 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1132-1152 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 659-669 |
|
| 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. | Mid-level-ontology.kif 29358-29358 | 3470.0 凯文度 是 锕 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29206-29206 | 2740.0 凯文度 是 铝 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29370-29370 | 2880.0 凯文度 是 銤 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29282-29282 | 2023.0 凯文度 是 锑 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29216-29216 | 87.29 凯文度 是 氩 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29246-29246 | 886.0 凯文度 是 砷 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29350-29350 | 610.0 凯文度 是 砹 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29292-29292 | 1913.0 凯文度 是 钡 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29188-29188 | 3243.0 凯文度 是 铍 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29346-29346 | 1833.0 凯文度 是 铋 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29190-29190 | 2823.0 凯文度 是 硼 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29250-29250 | 331.93 凯文度 是 溴 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29276-29276 | 1038.0 凯文度 是 镉 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29290-29290 | 963.0 凯文度 是 铯 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29220-29220 | 1760.0 凯文度 是 钙 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29192-29192 | 5100.0 凯文度 是 碳 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29296-29296 | 3530.0 凯文度 是 铈 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29214-29214 | 238.55 凯文度 是 氯 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29228-29228 | 2755.0 凯文度 是 铬 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29234-29234 | 3143.0 凯文度 是 钴 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29238-29238 | 2868.0 凯文度 是 铜 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29312-29312 | 2608.0 凯文度 是 镝 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29316-29316 | 2783.0 凯文度 是 铒 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29306-29306 | 1870.0 凯文度 是 铕 的 boiling 点 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29198-29198 | 85.01 凯文度 是 氟 的 boiling 点 |
| 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