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 4553-4557 | |
(domain SubtractionFn 1 Number) | Merge.kif 4549-4549 | The number 1 argument of subtraction is an instance of number |
(domain SubtractionFn 2 Number) | Merge.kif 4550-4550 | The number 2 argument of subtraction is an instance of number |
(identityElement SubtractionFn 0) | Merge.kif 5025-5025 | 0 is an identity element of subtraction |
(instance SubtractionFn BinaryFunction) | Merge.kif 4546-4546 | Subtraction is an instance of binary function |
(instance SubtractionFn TotalValuedRelation) | Merge.kif 4548-4548 | Subtraction is an instance of total valued relation |
(range SubtractionFn Number) | Merge.kif 4551-4551 | The range of subtraction is an instance of number |
appearance as argument number 2 |
![]() |
(format ChineseLanguage SubtractionFn "(%*[-])") | chinese_format.kif 684-684 | |
(format EnglishLanguage SubtractionFn "(%*[-])") | english_format.kif 689-689 | |
(termFormat ChineseLanguage SubtractionFn "减法") | domainEnglishFormat.kif 55844-55844 | |
(termFormat ChineseLanguage SubtractionFn "减法函数") | chinese_format.kif 685-685 | |
(termFormat ChineseTraditionalLanguage SubtractionFn "減法") | domainEnglishFormat.kif 55843-55843 | |
(termFormat EnglishLanguage SubtractionFn "subtraction") | domainEnglishFormat.kif 55842-55842 |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree)) |
Merge.kif 6731-6733 | A real number celsius degree(s) is equal to (the real number and 32) and 1.8 fahrenheit degree(s) |
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree)) |
Merge.kif 6727-6729 | 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 928-941 | 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 4559-4560 | For all an integer (the integer+2) is equal to (the integer and 1) |
![]() |
![]() |