  Browsing Interface : Welcome guest : log in [  Home |  Graph |  ]  KB:  SUMO Language:  AlbanianLanguageArabicLanguageBasqueLanguageBulgarianLanguageCatalanLanguageChinchimneyeseTraditionalLanguageChineseLanguageChineseTraditionalLanguageCroatianLanguageDanishLanguageEnglishLanguageFarsiLanguageFinnishLanguageFrenchLanguageGalicianLanguageGermanLanguageGreekLanguageHebrewLanguageIcelandicLanguageIndonesianLanguageItalianLanguageJapaneseLanguageMalayLanguageNorwegianBokmalLanguageNorwegianNorskLanguagePolishLanguagePortugueseLanguageSpanishLanguageSwedishLanguageTaiwanChineseLanguageThaiLanguagede   Formal Language:  OWLSUO-KIFTPTPtraditionalLogic

 KB Term: Term intersection English Word: Any Noun Verb Adjective Adverb

Sigma KEE - DivisionFn
 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) 会是为定义。") Merge.kif 7033-7036 (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 7027-7031 (documentation DivisionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (DivisionFn ?NUMBER1 ?NUMBER2) は ?NUMBER1を ?NUMBER2で除算した結果である。注１：?NUMBER1 = 1 (DivisionFn ?NUMBER1 ?NUMBER2) が ?NUMBER2 の逆数である場合がある。　注２：?NUMBER2 = 0 の場合、(DivisionFn ?NUMBER1 ?NUMBER2) は未定義である。") Merge.kif 7038-7041 (domain DivisionFn 1 Quantity) Merge.kif 7023-7023 The number 1 argument of division is an instance of quantity (domain DivisionFn 2 Quantity) Merge.kif 7024-7024 The number 2 argument of division is an instance of quantity (identityElement DivisionFn 1) Merge.kif 7664-7664 1 is an identity element of division (instance DivisionFn AssociativeFunction) Merge.kif 7020-7020 Division is an instance of associative function (instance DivisionFn BinaryFunction) Merge.kif 7019-7019 Division is an instance of binary function (instance DivisionFn PartialValuedRelation) Merge.kif 7022-7022 Division is an instance of partial valued relation (range DivisionFn Quantity) Merge.kif 7025-7025 The range of division is an instance of quantity

 appearance as argument number 2 (format ChineseLanguage DivisionFn "%*[/]") chinese_format.kif 686-686 (format EnglishLanguage DivisionFn "%*[/]") english_format.kif 949-949 (format JapaneseLanguage DivisionFn "%*[/]") english_format.kif 950-950 (termFormat ChineseLanguage DivisionFn "部") domainEnglishFormat.kif 19921-19921 "部" is the printable form of division in ChineseLanguage (termFormat ChineseLanguage DivisionFn "除法函数") chinese_format.kif 687-687 "除法函数" is the printable form of division in ChineseLanguage (termFormat ChineseTraditionalLanguage DivisionFn "部") domainEnglishFormat.kif 19920-19920 "部" is the printable form of division in ChineseTraditionalLanguage (termFormat EnglishLanguage DivisionFn "division") domainEnglishFormat.kif 19919-19919 "division" is the printable form of division in english language

 antecedent (=>     (and         (approximateDiameter ?O             (MeasureFn ?L ?LM))         (sphereRadius ?S             (MeasureFn                 (DivisionFn ?L 2) ?LM))         (measure ?S             (MeasureFn ?V1 ?VM))         (measure ?O             (MeasureFn ?V2 ?VM))         (instance ?LM LengthMeasure)         (instance ?VM VolumeMeasure))     (equal ?V1 ?V2)) Mid-level-ontology.kif 15653-15664 If the approximate diameter of a self connected object is a real number the real numberM(s) and the radius of an object is the real number and 2 the real numberM(s) and the measure of the object is another real number another unit of measure(s) and the measure of the self connected object is a third real number the other unit of measure(s) and the real numberM is an instance of length measure and the other unit of measure is an instance of volume measure,then the other real number is equal to the third real number (=>     (and         (irrigatedLandArea ?REGION             (MeasureFn ?AMOUNT ?UNIT))         (totalArea ?REGION             (MeasureFn ?TOTAL ?UNIT))         (instance ?UNIT UnitOfArea)         (equal ?FRACTION             (DivisionFn ?AMOUNT ?TOTAL)))     (irrigatedLandArea ?REGION ?FRACTION)) Geography.kif 2168-2174 If a real number an unit of measure(s) is an irrigated land area of a geographic area and another real number the unit of measure(s) is a total area of the geographic area and the unit of measure is an instance of UnitOfArea and a constant quantity is equal to the real number and the other real number,then the constant quantity is an irrigated land area of the geographic area (=>     (and         (irrigatedLandArea ?REGION ?AMOUNT)         (instance ?AMOUNT AreaMeasure)         (totalArea ?REGION ?TOTAL)         (instance ?TOTAL AreaMeasure)         (equal ?FRACTION             (DivisionFn ?AMOUNT ?TOTAL)))     (irrigatedLandArea ?REGION ?FRACTION)) Geography.kif 2159-2166 If a constant quantity is an irrigated land area of a geographic area and the constant quantity is an instance of area measure and an area measure is a total area of the geographic area and the area measure is an instance of area measure and another constant quantity is equal to the constant quantity and the area measure,then the other constant quantity is an irrigated land area of the geographic area (=>     (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 3535-3554 If the measure of an object is a real number lumen(s) and the measure of another object is another real number lumen(s) and the object is a part of a third object and the other object is a part of the third object and the object is not equal to the other object and the real number is greater than the other real number and the real number and the other real number is equal to a rational number and the contrast ratio of the third object is the rational number,then there don't exist a fourth object, a fifth object,, , a third real number and a fourth real number such that the measure of the fourth object is the third real number lumen(s) and the measure of the fifth object is the fourth real number lumen(s) and the fourth object is a part of the third object and the fifth object is a part of the third object and the fourth object is not equal to the fifth object and the third real number is greater than the fourth real number and the third real number and the fourth real number is greater than the rational number (=>     (and         (principalAmount ?Account ?Balance)         (fixedInterestRate ?Account ?Rate)         (compoundInterest ?Account ?Interest ?Period)         (equal ?Rate-Decimal             (DivisionFn ?Rate 100))         (equal ?Add             (AdditionFn 1 ?Rate-Decimal))         (equal ?Exponent             (ExponentiationFn ?Add                 (MagnitudeFn ?Period)))         (equal ?Multiply             (MultiplicationFn ?Exponent ?Balance)))     (equal ?Interest         (SubtractionFn ?Multiply ?Balance))) FinancialOntology.kif 532-541 If a currency measure is a principal amount of a financial account and an interest rate is a fixed interest rate of the financial account and the financial account compound interest an interest for a time interval and the interest rate-Decimal is equal to the interest rate and 100 and a real number is equal to (1 and the interest rate-Decimal) and another real number is equal to the real number raised to the power the magnitude of the time interval and a quantity is equal to the other real number and the currency measure,then the interest is equal to (the quantity and the currency measure) (=>     (and         (principalAmount ?Account ?Balance)         (fixedInterestRate ?Account ?Rate)         (simpleInterest ?Account ?Amount ?Period)         (equal ?Rate-Decimal             (DivisionFn                 (MagnitudeFn ?Rate) 100)))     (equal ?Amount         (MultiplicationFn             (MultiplicationFn                 (MagnitudeFn ?Period) ?Balance) ?Rate-Decimal))) FinancialOntology.kif 514-520 If a currency measure is a principal amount of a financial account and an interest rate is a fixed interest rate of the financial account and the financial account is simple interest an interest for a time interval and the interest rate-Decimal is equal to the magnitude of the interest rate and 100,then the interest is equal to the magnitude of the time interval and the currency measure and the interest rate-Decimal (=>     (and         (simpleInterest ?Account ?Interest ?Period)         (principalAmount ?Account ?Principal)         (equal ?Rate-Decimal             (DivisionFn ?Interest ?Principal))         (equal ?Rate             (MultiplicationFn ?Rate-Decimal 100)))     (interestRatePerPeriod ?Account ?Rate ?Period)) FinancialOntology.kif 551-557 If a financial account is simple interest an interest for a time interval and a currency measure is a principal amount of the financial account and an interest rate-Decimal is equal to the interest and the currency measure and the interest rate is equal to the interest rate-Decimal and 100,then the financial account is interest rate per period the interest rate for the time interval

 consequent statement (equal     (MeasureFn ?NUMBER AngularDegree)     (MeasureFn         (MultiplicationFn ?NUMBER             (DivisionFn Pi 180.0)) Radian)) Merge.kif 10757-10759 A real number angular degree(s) is equal to the real number and pi and 180.0 radian(s) (equal     (MeasureFn ?NUMBER CelsiusDegree)     (MeasureFn         (DivisionFn             (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree)) Merge.kif 10215-10217 A real number celsius degree(s) is equal to (the real number and 32) and 1.8 fahrenheit degree(s) (equal     (MeasureFn ?NUMBER Cup)     (MeasureFn         (DivisionFn ?NUMBER 2) Pint)) Merge.kif 10557-10559 A real number cup(s) is equal to the real number and 2 pint(s) (equal     (MeasureFn ?NUMBER Ounce)     (MeasureFn         (DivisionFn ?NUMBER 8) Cup)) Merge.kif 10570-10572 A real number ounce(s) is equal to the real number and 8 cup(s) (equal     (MeasureFn ?NUMBER Pint)     (MeasureFn         (DivisionFn ?NUMBER 2) Quart)) Merge.kif 10544-10546 A real number pint(s) is equal to the real number and 2 quart(s) (equal     (MeasureFn ?NUMBER Quart)     (MeasureFn         (DivisionFn ?NUMBER 4) UnitedStatesGallon)) Merge.kif 10531-10533 A real number quart(s) is equal to the real number and 4 united states gallon(s) (forall (?NUMBER)     (equal         (MeasureFn ?NUMBER OunceMass)         (MeasureFn             (DivisionFn ?NUMBER 16) PoundMass))) Mid-level-ontology.kif 10947-10950 For all a real number the real number Ounce(s) is equal to the real number and 16 pound mass(s) Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view) Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners