| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1359-1361 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 84-87 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 17-20 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 17-20 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 81-81 | 实例 的 1 数量 是 实体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 82-82 | 实例 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 80-80 | 实例 是 二元谓语 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 305-305 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 310-310 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 175-175 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 149-149 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1995-1995 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 127-127 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 173-173 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 400-400 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 188-188 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 195-195 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 184-184 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 302-302 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1281-1281 | 组员 和 实例 是 内部相关 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5399-5399 | 元素 是 实例 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 89-89 | 直接实例 是 实例 的 subrelation |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30256-30256 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 306-306 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30255-30255 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30254-30254 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 303-303 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1018-1022 | 有认知的主事 持有 account 金融账户 和 那个 有认知的主事 是 法人财团 的 instance 若且唯若 那个 金融账户 是 企业帐户 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 996-1000 | 有认知的主事 持有 account 金融账户 和 那个 有认知的主事 是 人类 的 instance 若且唯若 那个 金融账户 是 个人账户 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1462-1467 | 飞机 的 altitude 是 自身连接物体 和 那个 自身连接物体 是 行星地球 的 surface 和 那个 飞机 是 飞机 的 instance 若且唯若 高度测量 是 absolute 那个 飞机 的高度 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4754-4765 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0.0 和 那个 实数) |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2335-2340 | 金融账户 是 金融账户 的 instance 和 有认知的主事 possesses 金融资产 和 那个 金融账户 equal 那个 金融资产 的帐号 若且唯若 那个 有认知的主事 持有 account 那个 金融账户 |
| 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. | Mid-level-ontology.kif 30283-30293 | 实体 是 身体部位 的 instance 和 Bare 是 那个 实体 的 attribute 在 时间位置 holdsDuring 若且唯若 不存在 另一个 实体 这样 那个 另外 实体 是 服装 的 instance 和 covers 那个 另外 实体 and 那个 实体 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12357-12364 | 过程 是 结合 的 instance 和 客体 是 那个 过程 的 resource 和 实体 是 那个 过程 的 result 若且唯若 那个 客体 不 是 那个 实体 的 part 在 那个 过程 出现 的 time 的开始 holdsDuring 和 那个 客体 是 那个 实体 的 part 在 那个 过程 出现 的 time 的结束 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26427-26438 | 过程 是 Photocopying 的 instance 和 内容承载物理 是 那个 过程 的 patient 和 那个 内容承载物理 是 VisualContentBearingObject 的 instance 和 那个 内容承载物理 contains 命题 的资料 若且唯若 有存在 另一个 内容承载物理 和 另一个 命题 这样 那个 另外 内容承载物理 是 那个 过程 的 result 和 那个 另外 内容承载物理 是 VisualContentBearingObject 的 instance 和 那个 另外 内容承载物理 contains 那个 另外 命题 的资料 和 那个 命题 equal 那个 另外 命题 |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1789-1793 | 实体 是 WindowScrolling 的 instance 和 那个 实体 是 UserSignifiedGraphicalAction 的 instance 若且唯若 那个 实体 是 WindowScrollingByUser 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1832-1842 | 过程 是 退出 的 instance 和 金融账户 是 金融账户 的 instance 和 那个 金融账户 的 currency 是 那个 过程 的源头 和 不存在 另一个 过程 这样 那个 另外 过程 是 罚款 的 instance 和 那个 另外 过程 在 那个 金融账户 的 currency 结束 和 那个 过程 causes 那个 另外 过程 若且唯若 那个 金融账户 的 liqudity 是 高流动性 |
| 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 383-416 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 108-123 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 births equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 144-159 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千里的 deaths equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 264-290 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 429-462 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 336-368 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 182-213 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 migrants equal 实数 若且唯若 (那个 整数 和 另一个 整数) equal 1 和 实体 是 那个 另外 整数 year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 另外 实数 和 1000 equal 第三 实数 和 第三 整数 equal 符号串 所描述的类别 instance 的数量 和 第四 整数 equal 那个 符号串 所描述的类别 instance 的数量 和 (那个 第三 整数 和 那个 第四 整数) equal 第四 实数 和 那个 第四 实数 和 那个 第三 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 78-90 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 population 成长 equal 实数 若且唯若 (那个 整数 和 那个 整数P) equal 1 和 时间位置 是 那个 整数P year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 地缘政治区域 的 population equal 第三 实数 在 那个 时间位置 holdsDuring 和 那个 另外 实数 和 那个 第三 实数 equal 第四 实数 和 (那个 第四 实数 和 1) equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24870-24875 | PostalPlace 是 located 在 PostcodeArea 和 那个 PostalPlace 是 PostalPlace 的 instance 和 那个 PostcodeArea 是 PostcodeArea 的 instance 若且唯若 那个 PostalPlace 是在 post code 那个 PostcodeArea |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24843-24848 | PostalPlace 是 located 在 城市 和 那个 PostalPlace 是 PostalPlace 的 instance 和 那个 城市 是 城市 的 instance 若且唯若 那个 PostalPlace 是在 那个 城市 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24756-24761 | PostalPlace 是 located 在 Neighborhood 和 那个 PostalPlace 是 PostalPlace 的 instance 和 那个 Neighborhood 是 Neighborhood 的 instance 若且唯若 那个 PostalPlace 是在 那个 Neighborhood |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24827-24832 | PostalPlace 是 located 在 州或省 和 那个 PostalPlace 是 PostalPlace 的 instance 和 那个 州或省 是 州或省 的 instance 若且唯若 那个 PostalPlace 是在 那个 州或省 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24793-24800 | PostalPlace 是 located 在 地缘政治区域 和 那个 PostalPlace 是 PostalPlace 的 instance 和 那个 地缘政治区域 是 国家 的 instance 或 那个 地缘政治区域 是 依赖或特殊主权领域 的 instance 若且唯若 那个 PostalPlace 是在 那个 地缘政治区域 |
| 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. | FinancialOntology.kif 1018-1022 | 有认知的主事 持有 account 金融账户 和 那个 有认知的主事 是 法人财团 的 instance 若且唯若 那个 金融账户 是 企业帐户 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 996-1000 | 有认知的主事 持有 account 金融账户 和 那个 有认知的主事 是 人类 的 instance 若且唯若 那个 金融账户 是 个人账户 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4754-4765 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0.0 和 那个 实数) |
| 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. | Mid-level-ontology.kif 30283-30293 | 实体 是 身体部位 的 instance 和 Bare 是 那个 实体 的 attribute 在 时间位置 holdsDuring 若且唯若 不存在 另一个 实体 这样 那个 另外 实体 是 服装 的 instance 和 covers 那个 另外 实体 and 那个 实体 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26427-26438 | 过程 是 Photocopying 的 instance 和 内容承载物理 是 那个 过程 的 patient 和 那个 内容承载物理 是 VisualContentBearingObject 的 instance 和 那个 内容承载物理 contains 命题 的资料 若且唯若 有存在 另一个 内容承载物理 和 另一个 命题 这样 那个 另外 内容承载物理 是 那个 过程 的 result 和 那个 另外 内容承载物理 是 VisualContentBearingObject 的 instance 和 那个 另外 内容承载物理 contains 那个 另外 命题 的资料 和 那个 命题 equal 那个 另外 命题 |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 1789-1793 | 实体 是 WindowScrolling 的 instance 和 那个 实体 是 UserSignifiedGraphicalAction 的 instance 若且唯若 那个 实体 是 WindowScrollingByUser 的 instance |
| No TPTP formula. May not be expressible in strict first order. | People.kif 383-416 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 108-123 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 births equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 144-159 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千里的 deaths equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 264-290 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 429-462 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 336-368 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列， 另一个 整数,， ， 符号串,， ， 实体,， ， 另一个 实体， and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
| No TPTP formula. May not be expressible in strict first order. | People.kif 182-213 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 migrants equal 实数 若且唯若 (那个 整数 和 另一个 整数) equal 1 和 实体 是 那个 另外 整数 year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 另外 实数 和 1000 equal 第三 实数 和 第三 整数 equal 符号串 所描述的类别 instance 的数量 和 第四 整数 equal 那个 符号串 所描述的类别 instance 的数量 和 (那个 第三 整数 和 那个 第四 整数) equal 第四 实数 和 那个 第四 实数 和 那个 第三 实数 equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 78-90 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 population 成长 equal 实数 若且唯若 (那个 整数 和 那个 整数P) equal 1 和 时间位置 是 那个 整数P year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 地缘政治区域 的 population equal 第三 实数 在 那个 时间位置 holdsDuring 和 那个 另外 实数 和 那个 第三 实数 equal 第四 实数 和 (那个 第四 实数 和 1) equal 那个 实数 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1533-1538 | 1 对于 %3 在周期 %2 的 annual 地区消费 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 货币测量 是 地缘政治区域 在 annual 地区消费 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1504-1509 | 地缘政治区域 annual 对于 有点 时距 在周期 货币测量 的地区收入 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 annual 地区收入 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 723-734 | 和弦音乐 是 客体 的 attribute 若且唯若 有存在 过程 和 另一个 过程 这样 那个 客体 是 制作音乐 的 instance 和 那个 过程 是 制作音乐 的 instance 和 那个 另外 过程 是 制作音乐 的 instance 和 那个 过程%n是那个 客体的subProcess 和 那个 另外 过程%n是那个 客体的subProcess 和 那个 过程 不 equal 那个 另外 过程 和 那个 过程 和 那个 客体 同时发生 和 那个 另外 过程 和 那个 客体 同时发生 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 4614-4622 | 公海 是 客体 的 attribute 若且唯若 那个 客体 是 盐水区 的 instance 和 那个 客体 不 是 内陆水域 的 instance 和 物理 和 那个 客体 的 distance 是 实数 海里 和 那个 实数 是 greaterThan 5.0 |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3956-3961 | 银行 - 财政组织 是 有点 金融账户 的 bank 帐号 若且唯若 有存在 另一个 金融账户 这样 那个 另外 金融账户 是 有点 金融账户 的 instance 和 那个 另外 金融账户 是被 那个 银行 - 财政组织 held |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1581-1586 | 地缘政治区域 在周期 货币测量 对于 有点 时距 的 capital 地区支出 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 capital 地区支出 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3677-3682 | 有点 时距 是 货币测量 的 currency 交换 每美元 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 美国美元 的 currency 交换汇率 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3684-3689 | UnitOfCurrency 对于 有点 时距 在周期 货币测量 的 currency 交换汇率 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 UnitOfCurrency 的 currency 交换汇率 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7694-7700 | 施事体 是 有认知的主事 的 customer 若且唯若 有存在 过程 这样 那个 过程 是 金融交易 的 instance 和 那个 施事体 是 那个 过程 的 agent 和 那个 过程 在 那个 有认知的主事 结束 |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3648-3655 | 有认知的主事 对于 %3 的 customer 代表 若且唯若 有存在 过程 这样 那个 过程 是 金融交易 的 instance 和 机构 employs 那个 有认知的主事 和 那个 有认知的主事 是 那个 过程 的 agent 和 那个 过程 在 另一个 有认知的主事 结束 |
| 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. | Geography.kif 3119-3119 | ?D 是 23 Day 的 instance 是 南极条约 的 agreement 生效日期 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 482-495 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每个女人生的 children equal 符号串 所描述的类别 instance 的数量 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1241-1248 | 对所有 ?AGENT， ?VOTER,， ， ?ELECTION， and 和 ?VOTING
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 923-931 | 对所有 ?COUNTRY， ?ELECTION,， ， ?VOTING， and 和 ?VOTER
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1092-1103 | 对所有 ?POLITY， ?AGENT,， ， ?ELECTION,， ， ?VOTINGAGE， and 和 ?AGE
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1160-1174 | 对所有 ?POLITY， ?VOTER,， ， ?ELECTION,， ， ?VOTINGAGE， and 和 ?AGE
|
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 921-929 | ?SYMPTOM 是 ?AGENT 的 biochemical 病毒征兆 和 ?AGENT biochemical 病毒解毒制剂 ?SUBSTANCE 对于 ?PROCESS 和 ?SAMPLE 是 ?SUBSTANCE 的 instance 和 ?THERAPY 是 ?PROCESS 的 instance 和 ?ORGANISM 经历了 ?THERAPY 和 ?SAMPLE 是 ?THERAPY 的 patient 减少 ?SYMPTOM 是 ?ORGANISM 的 attribute 发生的机率 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18042-18059 | 有存在 ?X， ?CUT,， ， ?PAPER,， ， ?CBO， and 和 ?INFO 这样 ?X 是 PaperShredder 的 instance 和 ?CUT 是 切开 的 instance 和 ?X 是导致 ?CUT 的 instrument 和 ?PAPER 是 纸 的 instance 和 ?PAPER 是 ?CUT 的 patient 和 ?CBO 是 located 在 ?PAPER 和 ?CBO 是 VisualContentBearingObject 的 instance 和 ?CBO contains ?INFO 的资料 减少 有存在 ?READ 这样 ?READ 是 解读 的 instance 和 ?INFO 是 ?READ 的 patient 和 ?CUT 出现 的 time 比?READ 出现 的 time发生的earlier 发生的机率 |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 872-881 | 地缘政治区域 的 available 军事服务男性 equal 符号串 所描述的类别 instance 的数量 |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 895-906 | 地缘政治区域 的 fit 对于军服务男性 equal 符号串 所描述的类别 instance 的数量 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 49-54 | 地缘政治区域 的 population equal 符号串 所描述的类别 instance 的数量 |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 933-946 | 地缘政治区域 和 年 每年的 reaching 军事男性年龄 equal 符号串 所描述的类别 instance 的数量 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2453-2457 | 有存在 时间位置 这样 那个 时间位置 是 1976 year 的 instance 和 斯蒂夫·沃兹尼亚克 是 史蒂芬·贾伯斯 的 coworker 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2441-2445 | 有存在 时间位置 这样 那个 时间位置 是 2002 year 的 instance 和 提姆·库克 是 史蒂芬·贾伯斯 的 coworker 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 825-826 | 有存在 实体 这样 那个 实体 是 实体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3307-3313 | IBookstore 的 目的 是 有存在 ?D 这样 ?D 是 下載 的 instance 和 iBookstore 是导致 ?D 的 instrument 和 ?T 是 文本 的 instance 和 objectTransferred ?D and ?T |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2501-2504 | Serbia 是 欧洲国家 的 instance 和 时间位置 是 5 day 的 instance 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2496-2499 | Serbia 是 独立国家 的 instance 和 时间位置 是 5 day 的 instance 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2506-2509 | Serbia 的名 是 "Republic of Serbia" 和 时间位置 是 5 day 的 instance 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2528-2531 | 时间位置 是 3 day 的 instance 和 Montenegro 是 欧洲国家 的 instance 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2523-2526 | 时间位置 是 3 day 的 instance 和 Montenegro 是 独立国家 的 instance 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2533-2536 | 时间位置 是 3 day 的 instance 和 Montenegro 的名 是 "Montenegro" 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2546-2550 | 时间位置 是 3 day 的 instance 和 塞尔维亚和黑山 不 是 独立国家 的 instance 在 那个 时间位置 之后 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2791-2794 | 时间位置 是 1 day 的 instance 和 安第斯国际社会 是 "Andean Community of Nations" 的 conventional 全名 在 紧接 那个 时间位置 after holdsDuring |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 663-663 | 细胞 和 有点 细胞部分 的 cell 部分 是 有点 细胞部分 的 instance |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 652-652 | 病毒 和 有点 病毒部分 的 viral 部分 是 有点 病毒部分 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2534-2534 | AAA评级 是 财务评级 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3426-3426 | ABPFn 是 一元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4623-4623 | ABTest 是 ExperimentAttribute 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5379-5379 | 一种 pucikwar 语言 是 中央伟大的andamanese语言 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2874-2874 | 东盟区域论坛 是 国际组织 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3471-3471 | ASPFn 是 一元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2122-2122 | ATandTCorp 是 法人财团 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2560-2560 | AalandIslands 是 群岛 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2561-2561 | AalandIslands 是 依赖或特殊主权领域 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3771-3771 | Aariya语言 是 非语言口语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | People.kif 1235-1235 | 方丈 是 宗教立场 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 2923-2923 | Abinomn语言 是 口语人类语言 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3777-3777 | Abishira语言 是 非语言口语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14550-14550 | AbkhazLanguage 是 北方白种人语言 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2410-2410 | 中止 是 二元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2476-2476 | 中止发射 是 二元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2430-2430 | 任务中止 是 二元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16957-16957 | 以上 是 AntiSymmetricPositionalAttribute 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16956-16956 | 以上 是 位置属性 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4747-4747 | 绝对值函数 是 总值关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4746-4746 | 绝对值函数 是 一元函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13713-13713 | Abun语言 是 北鸟头语 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 518-518 | Acapella 是 MusicGenre 的 instance |
| 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