AbsoluteValueFn |
appearance as argument number 1 |
appearance as argument number 2 |
(format ChineseLanguage AbsoluteValueFn "%1 的绝对值") | chinese_format.kif 688-688 | |
(format EnglishLanguage AbsoluteValueFn "the absolute value of %1") | english_format.kif 690-690 | |
(format FrenchLanguage AbsoluteValueFn "la valeur absolue de %1") | french_format.kif 417-417 | |
(format ItalianLanguage AbsoluteValueFn "ilvalore assoluto di%1") | relations-it.txt 18-18 | |
(format JapaneseLanguage AbsoluteValueFn "%1 の absolute value") | japanese_format.kif 2134-2134 | |
(format PortugueseLanguage AbsoluteValueFn "o valor absoluto de %1") | portuguese_format.kif 369-369 | |
(format de AbsoluteValueFn "der absolutebetrag von %1") | relations-de.txt 895-895 | |
(format hi AbsoluteValueFn "%1 kaa nirapeksha maana") | relations-hindi.txt 63-63 | |
(format ro AbsoluteValueFn "value%t{valoarea} absolute{absolutã} a lui %1") | relations-ro.kif 439-439 | |
(format sv AbsoluteValueFn "absolutbeloppet av %1") | relations-sv.txt 461-461 | |
(format tg AbsoluteValueFn "ang buong kahulugan sa %1") | relations-cb.txt 52-52 | |
(termFormat ChineseLanguage AbsoluteValueFn "绝对值") | domainEnglishFormat.kif 5159-5159 | |
(termFormat ChineseLanguage AbsoluteValueFn "绝对值函数") | chinese_format.kif 689-689 | |
(termFormat ChineseTraditionalLanguage AbsoluteValueFn "絕對值") | domainEnglishFormat.kif 5158-5158 | |
(termFormat EnglishLanguage AbsoluteValueFn "absolute value") | domainEnglishFormat.kif 5157-5157 | |
(termFormat tg AbsoluteValueFn "tungkulin ng buong kahulugan") | relations-tg.txt 53-53 |
antecedent |
(<=> (and (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber)) (or (and (instance ?NUMBER1 NonnegativeRealNumber) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeRealNumber) (equal ?NUMBER2 (SubtractionFn 0.0 ?NUMBER1))))) |
Merge.kif 4769-4780 | 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) |