TreeView Knowledge Base Browser - AdditionFn

Browsing Interface : Welcome guest : log in

[ Home | Graph | ] KB: Language:
Formal Language:

KB Term:			Term intersection

English Word:

Sigma KEE - AdditionFn

AdditionFn

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2214-2215
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4620-4622
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4616-4616	The number 1 argument of addition is an instance of real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4617-4617	The number 2 argument of addition is an instance of real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5195-5195	0 is an identity element of addition
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4612-4612	Addition is an instance of associative function
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4611-4611	Addition is an instance of binary function
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4613-4613	Addition is an instance of commutative function
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4615-4615	Addition is an instance of total valued relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4618-4618	The range of addition 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 682-682
No TPTP formula. May not be expressible in strict first order.	english_format.kif 684-684
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 5427-5427
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 683-683
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 5426-5426
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 5425-5425

antecedent

No TPTP formula. May not be expressible in strict first order.	Media.kif 3056-3077	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.	Mid-level-ontology.kif 23355-23372	If menopause is an attribute of a human holds during a time interval and a real number is a birthdate of the human and another real number is equal to (year duration 49 and the real number) and a third real number is equal to (year duration 52 and the real number) and a time point is equal to the beginning of the time interval, then the statement the time point is greater than the other real number and the third real number is greater than the time point has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 436-453	If a financial transaction is an instance of deposit and a financial account is an instance of financial account and the financial transaction ends up at the currency of 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.	Weather.kif 1934-1943	If a list is an instance of consecutive time interval list and a time interval is equal to an entity element of the list and another time interval is equal to (a positive integer and 1)th element of the list, then the beginning of the other time interval is equal to the end of the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5021-5032	If an integer is not equal to 0 and (the largest integer less than or equal to another integer and the integer and the integer and a third integer) is equal to the other integer, then the other integer mod the integer is equal to the third integer

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 289-310	A real number is an average of a list if and only if there exists another list 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 a positive integer if the positive integer is a member of the other list, then there exist another real number, the other real numberMINUSONE,, , another positive integer and a third 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 positive integerth element of the other list is equal to the other real number and the other positive integer is a member of the list and the other real number is equal to the other positive integerth element of the list and the third 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 third positive integerth element of the other list and the positive integer is equal to (the other positive integer and the third positive integer) and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5891-5904	If the value of a graph path is equal to a real number and a graph arc is a part of the graph path and another graph arc is a part of the graph path and the value of the graph arc is another real number and the value of the other graph arc is a third real number and for all a graph element if the graph element is a part of the graph path, then the graph element is equal to the graph arc or the graph element is equal to the other graph arc , then the value of the graph path is equal to (the other real number and the third real number)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5877-5889	If the value of a graph path is equal to a real number and another graph path is a subgraph of the graph path and a graph arc is a part of the graph path and the value of the graph arc is another real number and for all a graph element if the graph element is a part of the graph path, then the graph element is a part of the other graph path or the graph element is equal to the graph arc , then the real number is equal to (the value of the other graph path and the other real number)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5008-5019	If an integer mod another integer is equal to a third integer and the other integer is not equal to 0, then (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3187-3197	If a real number is equal to the sum of a list and length of the list is greater than 1, then the real number is equal to (the first of the list and the sum of the sub-list from 2 to length of the list of the list)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3011-3030	If a list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list and a positive integer is less than or equal to length of the other list and another positive integer is less than or equal to length of the third list and the positive integer is an instance of positive integer and the other positive integer is an instance of positive integer, then the positive integerth element of the list is equal to the positive integerth element of the other list and (length of the other list and the other positive integer)th element of the list is equal to the other positive integerth element of the third list
No TPTP formula. May not be expressible in strict first order.	Media.kif 3056-3077	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 3118-3130	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.	Weather.kif 1452-1464	If a real number is equal to VarianceAverageFn of a list with the mean of a number and length of the list is greater than 1, then the real number is equal to (VarianceAverageFn of 1th element of the list with the mean of the number and VarianceAverageFn of the sub-list from 2 to length of the list of the list with the mean of the number)
No TPTP formula. May not be expressible in strict first order.	Geography.kif 562-567	If an unit of measure is an instance of UnitOfArea and a real number the unit of measure(s) is a land area only of a geographic area and another real number the unit of measure(s) is a water area only of the geographic area, then (the real number and the other real number) the unit of measure(s) is a total area of the geographic area
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 510-517	If a real number an unit of measure(s) is a total length of highway system of a geographic area and the real number1 the unit of measure(s) is a length of paved highway of the geographic area and the real number2 the unit of measure(s) is a length of unpaved highway of the geographic area and the unit of measure is an instance of UnitOfLength, then (the real number1 and the real number2) the unit of measure(s) is a total length of highway system of the geographic area
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 503-508	If a real number an unit of measure(s) is a total length of highway system of a geographic area and the real number1 the unit of measure(s) is a length of paved highway of the geographic area and the real number2 the unit of measure(s) is a length of unpaved highway of the geographic area, then the real number is equal to (the real number1 and the real number2)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6170-6178	If a compound substance is a conjugate of another compound substance, then there exist a positive integer and another positive integer such that the positive integer is a proton number of the other compound substance and the other positive integer is a proton number of the compound substance and the positive integer is equal to (the other positive integer and 1) or the other positive integer is equal to (the positive integer and 1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16934-16946	If the time the hour a nonnegative integer in zone central time zone is equal to the hour another nonnegative integer, then the other nonnegative integer is equal to (the nonnegative integer and 6)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16952-16964	If the time the hour a nonnegative integer in zone eastern time zone is equal to the hour another nonnegative integer, then the other nonnegative integer is equal to (the nonnegative integer and 5)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16916-16928	If the time the hour a nonnegative integer in zone mountain time zone is equal to the hour another nonnegative integer, then the other nonnegative integer is equal to (the nonnegative integer and 7)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16898-16910	If the time the hour a nonnegative integer in zone pacific time zone is equal to the hour another nonnegative integer, then the other nonnegative integer is equal to (the nonnegative integer and 8)

statement

No TPTP formula. May not be expressible in strict first order.

Merge.kif 4624-4625

For all an integer (the integer+1) is equal to (the integer and 1)

Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree

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