SubtractionFn - Sigma Knowledge base Browser

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	If a financial account current account balance a day for a real number united states dollar(s) and the real number is less than 0 and equal another real number and (0 and the real number), then the financial account is overdraft the other real number united states dollar(s) for the day
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 820-830	If a real number an unit of measure(s) is a down payment of a loan and an object is a loan for purchase of the loan and value of the object is another real number the unit of measure(s) and equal a third real number and (the other real number and the real number), then the third real number the unit of measure(s) is an original balance of the loan
No TPTP formula. May not be expressible in strict first order.	Media.kif 3052-3073	If equal a symbolic string and the reverse of another symbolic string and equal a nonnegative integer and the length of the other symbolic string and the nonnegative integer is greater than 1 and another nonnegative integer is greater than 0 and the other nonnegative integer is less than the nonnegative integer and equal an integer and the ceiling of (the nonnegative integer and 1) and 2 and equal the other nonnegative integerEW and ((the integer and the other nonnegative integer) and the integer) and equal a third symbolic string and the sub-string of the other symbolic string from the other nonnegative integer to (1 and the other nonnegative integer), then equal the third symbolic string and the sub-string of the symbolic string from the other nonnegative integerEW to (1 and the other nonnegative integerEW)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3183-3190	If equal a list and the sub-list from an integer to another integer of another list and equal (the other integer and the integer) and 0, then equal the list and null list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3192-3201	If equal a list and the sub-list from a positive integer to an integer of another list and equal (the integer and the positive integer) and 1, then equal the list and (the positive integerth element of the other list)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3203-3215	If equal a list and the sub-list from a positive integer to an integer of another list and (the integer and the positive integer) is greater than 1, then equal the list and the list composed of (the positive integerth element of the other list) and the sub-list from (1 and the positive integer) to the integer of the other list
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 25535-25549	If menopause is an attribute of an agent holds during a time interval and equal a real number and (1 year duration(s) and the beginning of the time interval) and equal another time interval and interval between the other time interval and the beginning of the time interval, then there doesn't exist a process such that the process is an instance of menstruation and the agent experiences the process
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3348-3358	If a human is income earned a real number an unit of measure(s) for an organizational process and another real number the unit of measure(s) is the amount charged in a charging a fee and the organizational process causes the charging a fee and equal a third real number and (the real number and the other real number), then the after tax income derived by the human from the organizational process is the third real number the unit of measure(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8716-8721	If a time interval is an instance of the day a positive integer of month a kind of month and another time interval is an instance of the day another positive integer of month a kind of month and equal (the other positive integer and the positive integer) and 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1930-1946	If a process is an instance of strong gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal a third real number and (the real number and the other real number), then the third real number is greater than 17 and the third real number is less than or equal to 29
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1953-1967	If a process is an instance of violent gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal a third real number and (the real number and the other real number), then the third real number is greater than 29
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1907-1923	If a process is an instance of weak gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal a third real number and (the real number and the other real number), then the third real number is greater than or equal to 12 and the third real number is less than or equal to 17
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1886-1900	If a process is an instance of wind gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and the time of existence of the process happens earlier than a time interval and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal a third real number and (the real number and the other real number), then the third real number is greater than or equal to 10
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1868-1884	If a process is an instance of wind gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal a third real number and (the real number and the other real number), then the real number is greater than or equal to 18 and the third real number is greater than or equal to 10
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8742-8747	If a time interval is an instance of the hour a nonnegative integer and another time interval is an instance of the hour another nonnegative integer and equal (the other nonnegative integer and the nonnegative integer) and 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8769-8774	If a time interval is an instance of the minute a nonnegative integer and another time interval is an instance of the minute another nonnegative integer and equal (the other nonnegative integer and the nonnegative integer) and 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 410-426	If a financial transaction is an instance of payment and the financial transaction originates at the currency of a financial account and the financial account is an instance of financial account and a real number an unit of measure(s) is a transaction amount of the financial transaction and the financial account current account balance immediately before the time of existence of the financial transaction for another real number the unit of measure(s) and equal a third real number and (the other real number and the real number), then the financial account current account balance immediately after the time of existence of the financial transaction for the third real number the unit of measure(s)
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1820-1837	If a process is an instance of squall and the process is located at an object and the object is an instance of geographic area and a real number miles per hour(s) is a surface wind speed of the object holds during the time of existence of the process and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the object holds during the time interval and equal a third real number and (the real number and the other real number), then the real number is greater than or equal to 25 and the third real number is greater than or equal to 18
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8796-8801	If a time interval is an instance of the second a positive integer and another time interval is an instance of the second another positive integer and equal (the other positive integer and the positive integer) and 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 468-483	If a financial transaction is an instance of withdrawing from an account and a financial account is an instance of financial account and the financial transaction originates at the financial account and a real number an unit of measure(s) is a transaction amount of the financial transaction and the financial account current account balance immediately before the time of existence of the financial transaction for another real number the unit of measure(s) and equal a third real number and (the other real number and the real number), then the financial account current account balance immediately after after the financial transaction for the third real number the unit of measure(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8861-8866	If a time interval is an instance of the year an integer and another time interval is an instance of the year another integer and equal (the other integer and the integer) and 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1028-1037	If an object is outside to a region and another object is an instance of the perimeter area of the region and the other object is an instance of uniform perimeter area and the width of the other object is a real number an unit of measure(s) and the distance between the object and the region is another real number the unit of measure(s) and the unit of measure is an instance of unit of measure and (the other real number and the real number) is greater than 0.0, then the object is not located at the other object
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1017-1026	If an object is outside to a region and another object is an instance of the perimeter area of the region and the other object is an instance of uniform perimeter area and the width of the other object is a real number an unit of measure(s) and the distance between the object and the region is another real number the unit of measure(s) and the unit of measure is an instance of unit of measure and (the other real number and the real number) is less than or equal to 0.0, then the object is located at the other object

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 if the other positive integer is a member of the other list, then there exist another real number, the other real numberMINUSONE,, , a third positive integer and a fourth positive integer such that the other real number is greater than 1 and the other real number is less than or equal to length of the other list and equal the other positive integerth element of the other list and the other real number and the third positive integer is a member of the list and equal the other real number and the third positive integerth element of the list and the fourth positive integer is a member of the other list and equal the other real numberMINUSONE and (the other real number and 1) and equal the other real numberMINUSONE and the fourth positive integerth element of the other list and equal the other positive integer and (the third positive integer and the fourth 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	If equal a real number and VarianceAverageFn of a list with the mean of another real number and equal 1 and length of the list, then equal the real number and (the other real number and 1th element of the list) and (the other real number and 1th element of the list)
No TPTP formula. May not be expressible in strict first order.	Geography.kif 3966-3978	If an object is an instance of geographic area and the object is object geographic coordinates a latitude for a longitude and equal a real number angular degree(s) and Location on Earth at Latitude the latitude and Longitude the longitude has a magnetic declination of PlaneAngleMeasure. (+) denotes easterly declination, (-) denotes westerly declination. zero value means at the agonic line., then there exists another real number such that the other real number angular degree(s) is a headingWRT true north of the object and (the other real number and the real number) angular degree(s) is a headingWRT magnetic north of the object
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16210-16219	If a time position is an instance of the day a positive integer of month the month a kind of month and another time position is a part of week before fn the time position and the time position is a part of week after fn the other time position, then there exists another positive integer such that the other time position is an instance of the day the other positive integer of month the month a kind of month and equal the other positive integer and (the positive integer and 7)
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 4563-4571	If a real number is an instance of quantity and another real number is an instance of quantity, then equal the financial improvement percentage of the real number over the other real number and (the real number and the other real number) and the other real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18089-18114	If the relative angle between an object and another object is a real number and one end of the object is a third object and one end of the object is a fourth object and equal the third object and the fourth object and the length of the object is the real number1 an unit of measure(s) and the length of the other object is the real number2 the unit of measure(s) and the distance between the third object and a fifth object is the real number3 the unit of measure(s) and one end of the other object is the fifth object and one end of the other object is a sixth object and equal the fifth object and the sixth object and the third object doesn't meet the fifth object, then equal the real number and the arccosine of ((the real number3 and the real number3 and the real number1 and the real number1) and the real number2 and the real number2) and 2.0 and the real number1 and the real number2
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18692-18708	If a physical quantity amount as resource for the Process a process and the physical quantity is an instance of constant quantity and an object is a resource for the process and the measure of the object is a real number an unit of measure(s) holds during the beginning of the time of existence of the process and the measure of the object is another real number the unit of measure(s) holds during the end of the time of existence of the process, then equal the physical quantity and (the real number and the other real number) the unit of measure(s)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18748-18774	If a function quantity amount as resource for the Process a process and the function quantity is an instance of function quantity and an object is a resource for the process and equal the function quantity and the per of a real number an unit of measure(s) and another real number another unit of measure(s) and duration of the time of existence of the process is a third real number the other unit of measure(s) and the measure of the object is a fourth real number the unit of measure(s) holds during the beginning of the time of existence of the process and the measure of the object is a physical quantity the unit of measure(s) holds during the end of the time of existence of the process, then equal the physical quantity and (the fourth real number and the third real number and the real number and the other real number) the unit of measure(s)

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

KB Term:			Term intersection

English Word: