DivisionFn |
appearance as argument number 1 |
(documentation DivisionFn ChineseLanguage "如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (DivisionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER1 除 ?NUMBER2 的商。注:当 ?NUMBER1 = 1 时, (DivisionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER2 的倒数。也要注意的是当 ?NUMBER2 = 0 时, (DivisionFn ?NUMBER1?NUMBER2) 会是为定义。") | chinese_format.kif 2220-2223 | |
(documentation DivisionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (DivisionFn ?NUMBER1 ?NUMBER2) is the result of dividing ?NUMBER1 by ?NUMBER2. Note that when ?NUMBER1 = 1 (DivisionFn ?NUMBER1 ?NUMBER2) is the reciprocal of ?NUMBER2. Note too that (DivisionFn ?NUMBER1 ?NUMBER2) is undefined when ?NUMBER2 = 0.") | Merge.kif 4746-4750 | |
(documentation DivisionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (DivisionFn ?NUMBER1 ?NUMBER2) は ?NUMBER1を ?NUMBER2で除算した結果である。注1:?NUMBER1 = 1 (DivisionFn ?NUMBER1 ?NUMBER2) が ?NUMBER2 の逆数である場合がある。 注2:?NUMBER2 = 0 の場合、(DivisionFn ?NUMBER1 ?NUMBER2) は未定義である。") | japanese_format.kif 884-887 | |
(domain DivisionFn 1 RealNumber) | Merge.kif 4742-4742 | 除法函数 的 1 数量 是 实数 的 instance |
(domain DivisionFn 2 RealNumber) | Merge.kif 4743-4743 | 除法函数 的 2 数量 是 实数 的 instance |
(identityElement DivisionFn 1) | Merge.kif 5297-5297 | 1 是 除法函数 的单位元 |
(instance DivisionFn BinaryFunction) | Merge.kif 4739-4739 | 除法函数 是 二元函数 的 instance |
(instance DivisionFn PartialValuedRelation) | Merge.kif 4741-4741 | 除法函数 是 部分值关系 的 instance |
(range DivisionFn RealNumber) | Merge.kif 4744-4744 | 除法函数 的 range 是 实数 的实例 |
appearance as argument number 2 |
(format ChineseLanguage DivisionFn "%*[/]") | chinese_format.kif 686-686 | |
(format EnglishLanguage DivisionFn "%*[/]") | english_format.kif 688-688 | |
(format FrenchLanguage DivisionFn "%*[/]") | french_format.kif 416-416 | |
(format ItalianLanguage DivisionFn "%*[/]") | relations-it.txt 80-80 | |
(format JapaneseLanguage DivisionFn "%*[/]") | japanese_format.kif 2133-2133 | |
(format PortugueseLanguage DivisionFn "%*[/]") | portuguese_format.kif 368-368 | |
(format cz DivisionFn "%*[/]") | relations-cz.txt 425-425 | |
(format de DivisionFn "%*[/]") | relations-de.txt 893-893 | |
(format hi DivisionFn "%*[/]") | relations-hindi.txt 120-120 | |
(format ro DivisionFn "%*[/]") | relations-ro.kif 438-438 | |
(format sv DivisionFn "%*[/]") | relations-sv.txt 460-460 | |
(format tg DivisionFn "%*[/]") | relations-cb.txt 114-114 | |
(termFormat ChineseLanguage DivisionFn "部") | domainEnglishFormat.kif 19992-19992 | |
(termFormat ChineseLanguage DivisionFn "除法函数") | chinese_format.kif 687-687 | |
(termFormat ChineseTraditionalLanguage DivisionFn "部") | domainEnglishFormat.kif 19991-19991 | |
(termFormat EnglishLanguage DivisionFn "division") | domainEnglishFormat.kif 19990-19990 | |
(termFormat tg DivisionFn "tungkulin ng paghahatihati") | relations-tg.txt 176-176 |
antecedent |
(=> (and (approximateDiameter ?O (MeasureFn ?L ?LM)) (sphereRadius ?S (MeasureFn (DivisionFn ?L 2.0) ?LM)) (measure ?S (MeasureFn ?V1 ?VM)) (measure ?O (MeasureFn ?V2 ?VM)) (instance ?LM UnitOfLength) (instance ?VM UnitOfVolume)) (equal ?V1 ?V2)) |
Mid-level-ontology.kif 17948-17959 |
|
(=> (and (equal ?OUT (ReverseFn ?IN)) (equal ?LEN (StringLengthFn ?IN)) (greaterThan ?LEN 1) (greaterThan ?N 0) (lessThan ?N ?LEN) (equal ?PIVOT (CeilingFn (DivisionFn (SubtractionFn ?LEN 1) 2))) (equal ?NEW (AdditionFn (SubtractionFn ?PIVOT ?N) ?PIVOT)) (equal ?S (SubstringFn ?IN ?N (AdditionFn 1 ?N)))) (equal ?S (SubstringFn ?OUT ?NEW (AdditionFn 1 ?NEW)))) |
Media.kif 3068-3089 |
|
(=> (and (instance ?C CoffeeArabica) (measure ?C (MeasureFn ?X Gram)) (instance ?CC Caffeine) (part ?CC ?C) (measure ?CC (MeasureFn ?Y Gram)) (equal ?Z (DivisionFn ?Y ?X))) (and (greaterThanOrEqualTo ?Z 0.008) (lessThanOrEqualTo ?Z 0.014))) |
Economy.kif 4645-4658 | |
(=> (and (instance ?C CoffeeRobusta) (measure ?C (MeasureFn ?X Gram)) (instance ?CC Caffeine) (part ?CC ?C) (measure ?CC (MeasureFn ?Y Gram)) (equal ?Z (DivisionFn ?Y ?X))) (and (greaterThanOrEqualTo ?Z 0.017) (lessThanOrEqualTo ?Z 0.04))) |
Economy.kif 4669-4682 | |
(=> (and (irrigatedLandArea ?REGION (MeasureFn ?AMOUNT ?UNIT)) (instance ?UNIT UnitOfArea) (totalArea ?REGION (MeasureFn ?TOTAL ?UNIT)) (equal ?FRACTION (DivisionFn ?AMOUNT ?TOTAL))) (irrigatedLandArea ?REGION (MeasureFn ?FRACTION ?UNIT))) |
Geography.kif 2215-2225 | |
(=> (and (irrigatedLandArea ?REGION (MeasureFn ?AMOUNT ?UNIT)) (totalArea ?REGION (MeasureFn ?TOTAL ?UNIT)) (instance ?UNIT UnitOfArea) (equal ?FRACTION (DivisionFn ?AMOUNT ?TOTAL))) (irrigatedLandArea ?REGION (MeasureFn ?FRACTION ?UNIT))) |
Geography.kif 2227-2237 | |
(=> (and (measure ?P1 (MeasureFn ?N1 Lumen)) (measure ?P2 (MeasureFn ?N2 Lumen)) (part ?P1 ?O) (part ?P2 ?O) (not (equal ?P1 ?P2)) (greaterThan ?N1 ?N2) (equal (DivisionFn ?N1 ?N2) ?R) (contrastRatio ?O ?R)) (not (exists (?P3 ?P4 ?N3 ?N4) (and (measure ?P3 (MeasureFn ?N3 Lumen)) (measure ?P4 (MeasureFn ?N4 Lumen)) (part ?P3 ?O) (part ?P4 ?O) (not (equal ?P3 ?P4)) (greaterThan ?N3 ?N4) (greaterThan (DivisionFn ?N3 ?N4) ?R))))) |
ComputingBrands.kif 3735-3756 |
|
(=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5117-5128 | |
(=> (and (principalAmount ?Account (MeasureFn ?Balance ?CUNIT)) (fixedInterestRate ?Account ?Rate) (simpleInterest ?Account (MeasureFn ?Amount ?CUNIT) ?Period) (equal ?Rate-Decimal (DivisionFn ?Rate 100))) (equal ?Amount (MultiplicationFn ?Balance ?Rate-Decimal))) |
FinancialOntology.kif 538-548 | |
(=> (and (simpleInterest ?Account (MeasureFn ?Interest ?CUNIT) ?Period) (principalAmount ?Account (MeasureFn ?Principal ?CUNIT)) (equal ?Rate-Decimal (DivisionFn ?Interest ?Principal)) (equal ?Rate (MultiplicationFn ?Rate-Decimal 100.0))) (interestRatePerPeriod ?Account ?Rate ?Period)) |
FinancialOntology.kif 587-597 |
consequent |
statement |