SubtractionFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2216-2219 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4730-4734 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 880-883 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | 减法函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | 减法函数 的 2 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5296-5296 | 0 是 减法函数 的单位元 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4723-4723 | 减法函数 是 二元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4725-4725 | 减法函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4728-4728 | 减法函数 的 range 是 实数 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 684-684 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 686-686 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 415-415 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 285-285 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2132-2132 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 367-367 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 424-424 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 891-891 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 322-322 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 437-437 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 459-459 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 477-477 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55854-55854 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 685-685 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55853-55853 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55852-55852 |
antecedent |
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. | FinancialOntology.kif 818-828 | |
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 3170-3177 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3179-3188 | |
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. | Mid-level-ontology.kif 23889-23903 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3331-3341 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8603-8608 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8629-8634 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8656-8661 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 408-424 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8683-8688 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 466-481 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8748-8753 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 863-872 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 852-861 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0.0 和 那个 实数) |
No TPTP formula. May not be expressible in strict first order. | People.kif 156-187 | 年 是 整数 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 52-64 | 年 是 整数 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. | People.kif 272-293 | 实数 是 串列 的 average 若且唯若 有存在 另一个 串列 和 正整数 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1486-1497 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14837-14846 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4563-4571 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17906-17931 |
|
statement |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7012-7014 | 实数 摄氏度 equal (那个 实数 和 32.0) 和 1.8 华氏度 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7008-7010 | 实数 摄氏度 equal (那个 实数 和 273.15) 凯文度 |
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. | Merge.kif 4736-4737 | 对所有 整数 (那个 整数+2) equal (那个 整数 和 1) |