SubtractionFn - Sigma Knowledge base Browser

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 4743-4747
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 4739-4739	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 4740-4740	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 5309-5309	0 is an identity element of subtraction
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4736-4736	Subtraction is an instance of binary function
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4738-4738	Subtraction is an instance of total valued relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4741-4741	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 55887-55887
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 55886-55886
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 55885-55885
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 another real number is equal to (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 a third real number is equal to (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 a symbolic string is equal to the reverse of another symbolic string and a nonnegative integer is equal to 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 an integer is equal to the ceiling of (the nonnegative integer and 1) and 2 and the other nonnegative integerEW is equal to ((the integer and the other nonnegative integer) and the integer) and a third symbolic string is equal to the sub_string of the other symbolic string from the other nonnegative integer to (1 and the other nonnegative integer), then the third symbolic string is equal to 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 3168-3175	If a list is equal to the sub-list from an integer to another integer of another list and (the other integer and the integer) is equal to 0, then the list is equal to null list
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3177-3186	If a list is equal to the sub-list from a positive integer to an integer of another list and (the integer and the positive integer) is equal to 1, then the list is equal to (the positive integerth element of the other list)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3188-3200	If a list is equal to 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 the list is equal to 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 25554-25568	If menopause is an attribute of an agent holds during a time interval and a real number is equal to (1 year duration(s) and the beginning of the time interval) and another time interval is equal to 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 a third real number is equal to (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 8701-8706	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 (the other positive integer and the positive integer) is equal to 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8727-8732	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 (the other nonnegative integer and the nonnegative integer) is equal to 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8754-8759	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 (the other nonnegative integer and the nonnegative integer) is equal to 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 a third real number is equal to (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.	Merge.kif 8781-8786	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 (the other positive integer and the positive integer) is equal to 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 a third real number is equal to (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 8846-8851	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 (the other integer and the integer) is equal to 1, then the time interval meets the other time interval
No TPTP formula. May not be expressible in strict first order.	Geography.kif 858-867	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 847-856	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 4781-4792	The absolute value of a real number is equal to 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 the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (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 the migrants per thousand of a geopolitical area and the year is equal to a real number if and only if (the integer and another integer) is equal to 1 and an entity is an instance of the year the other integer and the population of the geopolitical area is equal to another real number holds during the year and the other real number and 1000 is equal to a third real number and a third integer is equal to the number of instances in the class described by a symbolic string and a fourth integer is equal to the number of instances in the class described by the symbolic string and (the third integer and the fourth integer) is equal to a fourth real number and the fourth real number and the third real number is equal to 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 the population growth of a geopolitical area and the year is equal to a real number if and only if (the integer and the integerP) is equal to 1 and a time position is an instance of the year the integerP and the population of the geopolitical area is equal to another real number holds during the year and the population of the geopolitical area is equal to a third real number holds during the time position and the other real number and the third real number is equal to a fourth real number and (the fourth real number and 1) is equal to 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 length of the other list is equal to length of the list and 1th element of the other list is equal to 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 the other positive integerth element of the other list is equal to the other real number and the third positive integer is a member of the list and the other real number is equal to the third positive integerth element of the list and the fourth positive integer is a member of the other list and the other real numberMINUSONE is equal to (the other real number and 1) and the other real numberMINUSONE is equal to the fourth positive integerth element of the other list and the other positive integer is equal to (the third positive integer and the fourth positive integer) and the positive integer is equal to length of the other list and the real number is equal to 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 1469-1480	If a real number is equal to VarianceAverageFn of a list with the mean of another real number and 1 is equal to length of the list, then the real number is equal to (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 3796-3808	If an object is an instance of geographic area and the object is object geographic coordinates a latitude for a longitude and a real number angular degree(s) is equal to 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 16228-16237	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 the other positive integer is equal to (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 the financial improvement percentage of the real number over the other real number is equal to (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 18074-18099	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 the third object is not equal to 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 the fifth object is not equal to the sixth object and the third object doesn't meet the fifth object, then the real number is equal to 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 18709-18725	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 the physical quantity is equal to (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 18765-18791	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 the function quantity is equal to 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 the physical quantity is equal to (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 7022-7024	A real number celsius degree(s) is equal to (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 7018-7020	A real number celsius degree(s) is equal to (the real number and 273.15) kelvin degree(s)
No TPTP formula. May not be expressible in strict first order.	Military.kif 991-1004	The reaching military age annually male of a geopolitical area and a year is equal to 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 4749-4750	For all an integer (the integer+2) is equal to (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