Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - SubtractionFn
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 整数 yearinstance 地缘政治区域那个 年 每一千的 migrants equal 实数 若且唯若 (那个 整数另一个 整数) equal 1 和 实体那个 另外 整数 yearinstance那个 地缘政治区域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 整数 yearinstance 地缘政治区域那个 年population 成长 equal 实数 若且唯若 (那个 整数那个 整数P) equal 1 和 时间位置那个 整数P yearinstance那个 地缘政治区域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 几个元素 和 对所有 另一个 正整数 那个 正整数 equal 那个 另外 串列 的长度 和 那个 实数 equal 那个 另外 串列 的第 那个 正整数 几个元素 和 那个 正整数
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)


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