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 4758-4762
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 4754-4754 The number 1 argument of subtraction is an instance of real number
No TPTP formula. May not be expressible in strict first order. Merge.kif 4755-4755 The number 2 argument of subtraction is an instance of real number
No TPTP formula. May not be expressible in strict first order. Merge.kif 5324-5324 0 is an identity element of subtraction
No TPTP formula. May not be expressible in strict first order. Merge.kif 4751-4751 Subtraction is an instance of binary function
No TPTP formula. May not be expressible in strict first order. Merge.kif 4753-4753 Subtraction is an instance of total valued relation
No TPTP formula. May not be expressible in strict first order. Merge.kif 4756-4756 The range of subtraction is an instance of real number

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 55858-55858
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 55857-55857
No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 55856-55856
No TPTP formula. May not be expressible in strict first order. terms-de.txt 264-264

antecedent
-------------------------


No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 785-790
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 820-830
No TPTP formula. May not be expressible in strict first order. Media.kif 3052-3073
No TPTP formula. May not be expressible in strict first order. Merge.kif 3183-3190
No TPTP formula. May not be expressible in strict first order. Merge.kif 3192-3201
No TPTP formula. May not be expressible in strict first order. Merge.kif 3203-3215
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 25535-25549
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3348-3358
No TPTP formula. May not be expressible in strict first order. Merge.kif 8716-8721
No TPTP formula. May not be expressible in strict first order. Weather.kif 1930-1946
No TPTP formula. May not be expressible in strict first order. Weather.kif 1953-1967
No TPTP formula. May not be expressible in strict first order. Weather.kif 1907-1923
No TPTP formula. May not be expressible in strict first order. Weather.kif 1886-1900
No TPTP formula. May not be expressible in strict first order. Weather.kif 1868-1884
No TPTP formula. May not be expressible in strict first order. Merge.kif 8742-8747
No TPTP formula. May not be expressible in strict first order. Merge.kif 8769-8774
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 410-426
No TPTP formula. May not be expressible in strict first order. Weather.kif 1820-1837
No TPTP formula. May not be expressible in strict first order. Merge.kif 8796-8801
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 468-483
No TPTP formula. May not be expressible in strict first order. Merge.kif 8861-8866
No TPTP formula. May not be expressible in strict first order. Geography.kif 1028-1037
No TPTP formula. May not be expressible in strict first order. Geography.kif 1017-1026

consequent
-------------------------


No TPTP formula. May not be expressible in strict first order. Merge.kif 4796-4807 equal the absolute value of a real number and a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and equal the real number and the nonnegative real number or the real number is an instance of negative real number and equal the nonnegative real number and (0.0 and the real number)
No TPTP formula. May not be expressible in strict first order. People.kif 156-187 A year is an instance of the year an integer and equal the migrants per thousand of a geopolitical area and the year and a real number if and only if equal (the integer and another integer) and 1 and an entity is an instance of the year the other integer and equal the population of the geopolitical area and another real number holds during the year and equal the other real number and 1000 and a third real number and equal a third integer and the number of instances in the class described by a symbolic string and equal a fourth integer and the number of instances in the class described by the symbolic string and equal (the third integer and the fourth integer) and a fourth real number and equal the fourth real number and the third real number and the real number
No TPTP formula. May not be expressible in strict first order. People.kif 52-64 A year is an instance of the year an integer and equal the population growth of a geopolitical area and the year and a real number if and only if equal (the integer and the integerP) and 1 and a time position is an instance of the year the integerP and equal the population of the geopolitical area and another real number holds during the year and equal the population of the geopolitical area and a third real number holds during the time position and equal the other real number and the third real number and a fourth real number and equal (the fourth real number and 1) and the real number
No TPTP formula. May not be expressible in strict first order. People.kif 272-293 A real number is an average of a list if and only if there exist another list and a positive integer such that equal length of the other list and length of the list and equal 1th element of the other list and 1th element of the list and for all another positive integer and equal the positive integer and length of the other list and equal the real number and the positive integerth element of the other list and the positive integer
No TPTP formula. May not be expressible in strict first order. Weather.kif 2211-2222
No TPTP formula. May not be expressible in strict first order. Geography.kif 3966-3978
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16210-16219
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 18089-18114
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 18692-18708
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 18748-18774

statement
-------------------------


No TPTP formula. May not be expressible in strict first order. Merge.kif 7037-7039 equal a real number celsius degree(s) and (the real number and 32.0) and 1.8 fahrenheit degree(s)
No TPTP formula. May not be expressible in strict first order. Merge.kif 7033-7035 equal a real number celsius degree(s) and (the real number and 273.15) kelvin degree(s)
No TPTP formula. May not be expressible in strict first order. Military.kif 1001-1014 equal the reaching military age annually male of a geopolitical area and a year and the number of instances in the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order. Merge.kif 4764-4765 For all an integer equal (the integer+2) and (the integer and 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