SubtractionFn |
appearance as argument number 1 |
![]() |
(documentation SubtractionFn ChineseLanguage "如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (SubtractionFn ?NUMBER1 ?NUMBER2) 就是 ?NUMBER1 和 ?NUMBER2 的算术差,即使 ?NUMBER1 减 ?NUMBER2,除了在 ?NUMBER1 等于0时,那么(SubtractionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER2 的负数。") | chinese_format.kif 2216-2219 | |
(documentation SubtractionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (SubtractionFn ?NUMBER1 ?NUMBER2) is the arithmetical difference between ?NUMBER1 and ?NUMBER2, i.e. ?NUMBER1 minus ?NUMBER2. An exception occurs when ?NUMBER1 is equal to 0, in which case (SubtractionFn ?NUMBER1 ?NUMBER2) is the negation of ?NUMBER2.") | Merge.kif 4634-4638 | |
(domain SubtractionFn 1 RealNumber) | Merge.kif 4630-4630 | The number 1 argument of subtraction is an instance of real number |
(domain SubtractionFn 2 RealNumber) | Merge.kif 4631-4631 | The number 2 argument of subtraction is an instance of real number |
(identityElement SubtractionFn 0) | Merge.kif 5196-5196 | 0 is an identity element of subtraction |
(instance SubtractionFn BinaryFunction) | Merge.kif 4627-4627 | Subtraction is an instance of binary function |
(instance SubtractionFn TotalValuedRelation) | Merge.kif 4629-4629 | Subtraction is an instance of total valued relation |
(range SubtractionFn RealNumber) | Merge.kif 4632-4632 | The range of subtraction is an instance of real number |
appearance as argument number 2 |
![]() |
(format ChineseLanguage SubtractionFn "(%*[-])") | chinese_format.kif 684-684 | |
(format EnglishLanguage SubtractionFn "(%*[-])") | english_format.kif 686-686 | |
(termFormat ChineseLanguage SubtractionFn "减法") | domainEnglishFormat.kif 55833-55833 | |
(termFormat ChineseLanguage SubtractionFn "减法函数") | chinese_format.kif 685-685 | |
(termFormat ChineseTraditionalLanguage SubtractionFn "減法") | domainEnglishFormat.kif 55832-55832 | |
(termFormat EnglishLanguage SubtractionFn "subtraction") | domainEnglishFormat.kif 55831-55831 |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32.0) 1.8) FahrenheitDegree)) |
Merge.kif 6916-6918 | A real number celsius degree(s) is equal to (the real number and 32.0) and 1.8 fahrenheit degree(s) |
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree)) |
Merge.kif 6912-6914 | A real number celsius degree(s) is equal to (the real number and 273.15) kelvin degree(s) |
(equal (ReachingMilitaryAgeAnnuallyMaleFn ?AREA ?YEAR) (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (attribute ?PERSON Male) (militaryAge ?AREA ?MILITARYAGE) (equal ?AGEMINUSONE (SubtractionFn ?AGE 1)) (holdsDuring ?YEAR (or (age ?PERSON ?AGEMINUSONE) (age ?PERSON ?AGE))) (equal ?AGE ?MILITARYAGE) (inhabits ?PERSON ?AREA))))) |
Military.kif 933-946 | 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 |
(forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1))) |
Merge.kif 4640-4641 | For all an integer (the integer+2) is equal to (the integer and 1) |
![]() |
![]() |