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 4410-4414 | |
(domain SubtractionFn 1 Quantity) | Merge.kif 4406-4406 | The number 1 argument of subtraction is an instance of quantity |
(domain SubtractionFn 2 Quantity) | Merge.kif 4407-4407 | The number 2 argument of subtraction is an instance of quantity |
(identityElement SubtractionFn 0) | Merge.kif 4883-4883 | 0 is an identity element of subtraction |
(instance SubtractionFn AssociativeFunction) | Merge.kif 4403-4403 | Subtraction is an instance of associative function |
(instance SubtractionFn BinaryFunction) | Merge.kif 4402-4402 | Subtraction is an instance of binary function |
(instance SubtractionFn TotalValuedRelation) | Merge.kif 4405-4405 | Subtraction is an instance of total valued relation |
(range SubtractionFn Quantity) | Merge.kif 4408-4408 | The range of subtraction is an instance of quantity |
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 55795-55795 | "减法" is the printable form of subtraction in ChineseLanguage |
(termFormat ChineseLanguage SubtractionFn "减法函数") | chinese_format.kif 685-685 | "减法函数" is the printable form of subtraction in ChineseLanguage |
(termFormat ChineseTraditionalLanguage SubtractionFn "減法") | domainEnglishFormat.kif 55794-55794 | "減法" is the printable form of subtraction in ChineseTraditionalLanguage |
(termFormat EnglishLanguage SubtractionFn "subtraction") | domainEnglishFormat.kif 55793-55793 | "subtraction" is the printable form of subtraction in english language |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree)) |
Merge.kif 6595-6597 | 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 6591-6593 | 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 4416-4417 | For all an integer (the integer+2) is equal to (the integer and 1) |
![]() |
![]() |