| 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 4556-4560 | |
| (domain DivisionFn 1 Quantity) | Merge.kif 4552-4552 | |
| (domain DivisionFn 2 Quantity) | Merge.kif 4553-4553 | |
| (identityElement DivisionFn 1) | Merge.kif 5013-5013 | |
| (instance DivisionFn BinaryFunction) | Merge.kif 4549-4549 | |
| (instance DivisionFn PartialValuedRelation) | Merge.kif 4551-4551 | |
| (range DivisionFn Quantity) | Merge.kif 4554-4554 |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage DivisionFn "%*[/]") | chinese_format.kif 686-686 | |
| (format EnglishLanguage DivisionFn "%*[/]") | english_format.kif 691-691 | |
| (termFormat ChineseLanguage DivisionFn "部") | domainEnglishFormat.kif 19915-19915 | |
| (termFormat ChineseLanguage DivisionFn "除法函数") | chinese_format.kif 687-687 | |
| (termFormat ChineseTraditionalLanguage DivisionFn "部") | domainEnglishFormat.kif 19914-19914 | |
| (termFormat EnglishLanguage DivisionFn "division") | domainEnglishFormat.kif 19913-19913 |
| 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 15678-15689 | |
| (=> (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 3036-3057 | |
| (=> (and (irrigatedLandArea ?REGION (MeasureFn ?AMOUNT ?UNIT)) (totalArea ?REGION (MeasureFn ?TOTAL ?UNIT)) (instance ?UNIT UnitOfArea) (equal ?FRACTION (DivisionFn ?AMOUNT ?TOTAL))) (irrigatedLandArea ?REGION ?FRACTION)) |
Geography.kif 2180-2186 | |
| (=> (and (irrigatedLandArea ?REGION ?AMOUNT) (instance ?AMOUNT AreaMeasure) (totalArea ?REGION ?TOTAL) (instance ?TOTAL AreaMeasure) (equal ?FRACTION (DivisionFn ?AMOUNT ?TOTAL))) (irrigatedLandArea ?REGION ?FRACTION)) |
Geography.kif 2171-2178 | |
| (=> (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 3710-3729 | |
| (=> (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 531-540 | |
| (=> (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 513-519 | |
| (=> (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 550-556 |
| consequent |
|
|
| (<=> (average ?LIST1 ?AVERAGE) (exists (?LIST2) (and (equal (ListLengthFn ?LIST2) (ListLengthFn ?LIST1)) (equal (ListOrderFn ?LIST2 1) (ListOrderFn ?LIST1 1)) (forall (?ITEMFROM2) (=> (inList ?ITEMFROM2 ?LIST2) (exists (?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2) (and (greaterThan ?POSITION 1) (lessThanOrEqualTo ?POSITION (ListLengthFn ?LIST2)) (equal (ListOrderFn ?LIST2 ?ITEMFROM2) ?POSITION) (inList ?ITEMFROM1 ?LIST1) (equal ?POSITION (ListOrderFn ?LIST1 ?ITEMFROM1)) (inList ?PRIORFROM2 ?LIST2) (equal ?POSITIONMINUSONE (SubtractionFn ?POSITION 1)) (equal ?POSITIONMINUSONE (ListOrderFn ?LIST2 ?PRIORFROM2)) (equal ?ITEMFROM2 (AdditionFn ?ITEMFROM1 ?PRIORFROM2)))))) (equal ?LASTPLACE (ListLengthFn ?LIST2)) (equal ?AVERAGE (DivisionFn (ListOrderFn ?LIST2 ?LASTPLACE) ?LASTPLACE))))) |
People.kif 285-306 | |
| (<=> (beliefGroupPercentInRegion ?BG ?N ?R) (exists (?G1 ?G2) (and (located ?P ?R) (member ?P ?BG) (member ?P ?G1) (memberCount ?G1 ?N1) (located ?P2 ?R) (member ?P2 ?G2) (memberCount ?G2 ?N2) (equal (DivisionFn ?N 100) (DivisionFn ?N1 ?N2))))) |
People.kif 1530-1541 | |
| (<=> (compressionRatio ?E ?R) (and (minCylinderVolume ?E (MeasureFn ?MIN ?M)) (maxCylinderVolume ?E (MeasureFn ?MAX ?M)) (equal ?R (DivisionFn ?MIN ?MAX)))) |
Cars.kif 1918-1923 | |
| (<=> (equal (BirthsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (DivisionFn (PopulationFn ?AREA) 1000) ?THOUSANDS) (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 104-117 | |
| (<=> (equal (DeathsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (DivisionFn (PopulationFn ?AREA) 1000) ?THOUSANDS) (equal ?DEATHCOUNT (CardinalityFn (KappaFn ?DEATH (and (instance ?DEATH Death) (experiencer ?DEATH ?PERSON) (instance ?PERSON Human) (during (WhenFn ?DEATH) (YearFn ?YEAR)) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?DEATHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 138-151 | |
| (<=> (equal (DeathsPerThousandLiveBirthsFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) (YearFn ?YEAR)) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT 1000) ?THOUSANDSOFBIRTHS) (equal ?INFANTDEATHCOUNT (CardinalityFn (KappaFn ?DEATH (and (instance ?DEATH Death) (experiencer ?DEATH ?INFANT) (instance ?INFANT Human) (age ?INFANT (MeasureFn ?AGE YearDuration)) (lessThan ?AGE 1) (during (WhenFn ?DEATH) (YearFn ?YEAR)) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?INFANTDEATHCOUNT ?THOUSANDSOFBIRTHS) ?REALNUMBER))) |
People.kif 253-277 | |
| (<=> (equal (MaleToFemaleRatioFn ?AREA) ?REALNUMBER) (and (equal ?MALECOUNT (CardinalityFn (KappaFn ?MALE (and (instance ?MALE Human) (attribute ?MALE Male) (inhabits ?MALE ?AREA))))) (equal ?FEMALECOUNT (CardinalityFn (KappaFn ?FEMALE (and (instance ?FEMALE Human) (attribute ?FEMALE Female) (inhabits ?FEMALE ?AREA))))) (equal (DivisionFn ?MALECOUNT ?FEMALECOUNT) ?REALNUMBER))) |
People.kif 221-238 | |
| (<=> (equal (MigrantsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (SubtractionFn ?YEAR ?PREVIOUSYEAR) 1) (holdsDuring (YearFn ?YEAR) (equal (PopulationFn ?AREA) ?POPULATION)) (equal (DivisionFn ?POPULATION 1000) ?THOUSANDS) (equal ?IMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring (YearFn ?PREVIOUSYEAR) (not (inhabits ?PERSON ?AREA))) (holdsDuring (YearFn ?YEAR) (inhabits ?PERSON ?AREA)))))) (equal ?EMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring (YearFn ?PREVIOUSYEAR) (inhabits ?PERSON ?AREA)) (holdsDuring (YearFn ?YEAR) (not (inhabits ?PERSON ?AREA))))))) (equal (SubtractionFn ?IMMIGRATION ?EMMIGRATION) ?MIGRATIONCOUNT) (equal (DivisionFn ?MIGRATIONCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 174-202 | |
| (<=> (equal (PopulationGrowthFn ?AREA (YearFn ?YEAR)) ?ADJUSTEDPERCENT) (and (equal (SubtractionFn ?YEAR ?PREVIOUSYEAR) 1) (holdsDuring (YearFn ?YEAR) (equal (PopulationFn ?AREA) ?POPULATION)) (holdsDuring (YearFn ?PREVIOUSYEAR) (equal (PopulationFn ?AREA) ?PREVIOUSPOPULATION)) (equal (DivisionFn ?POPULATION ?PREVIOUSPOPULATION) ?PERCENT) (equal (SubtractionFn ?PERCENT 1) ?ADJUSTEDPERCENT))) |
People.kif 77-86 | |
| (<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 4891-4893 | |
| (<=> (ethnicityPercentInRegion ?BG ?N ?R) (exists (?G1 ?G2) (and (located ?P ?R) (member ?P ?BG) (member ?P ?G1) (memberCount ?G1 ?N1) (located ?P2 ?R) (member ?P2 ?G2) (memberCount ?G2 ?N2) (equal (DivisionFn ?N 100) (DivisionFn ?N1 ?N2))))) |
People.kif 1549-1560 | |
| (<=> (languagePercentInRegion ?L ?N ?R) (exists (?G1 ?G2) (and (located ?P ?R) (member ?P ?G1) (speaksLanguage ?P ?L) (memberCount ?G1 ?N1) (located ?P2 ?R) (member ?P2 ?G2) (memberCount ?G2 ?N2) (equal (DivisionFn ?N 100) (DivisionFn ?N1 ?N2))))) |
People.kif 1568-1579 | |
| (<=> (measure ?OBJECT (MeasureFn ?NUMBER OunceMass)) (measure ?OBJECT (MeasureFn (DivisionFn ?NUMBER 16) PoundMass))) |
Mid-level-ontology.kif 10970-10975 | |
| (=> (and (equal ?A (AverageFn ?L)) (greaterThan (ListLengthFn ?L) 0)) (equal ?A (DivisionFn (ListSumFn ?L) (ListLengthFn ?L)))) |
Merge.kif 3161-3168 | |
| (=> (and (equal ?V (VarianceFn ?L)) (equal ?M (AverageFn ?L))) (equal ?V (DivisionFn (VarianceAverageFn ?M ?L) (ListLengthFn ?L)))) |
Weather.kif 1078-1087 | |
| (=> (and (instance ?BTS BimetalTemperatureSensor) (instance ?M1 Metal) (instance ?M2 Metal) (not (equal ?M1 ?M2)) (part ?M1 ?BTS) (part ?M2 ?BTS) (instance ?T1 TemperatureMeasure) (instance ?T2 TemperatureMeasure) (instance ?L1 LengthMeasure) (instance ?L2 LengthMeasure) (instance ?L3 LengthMeasure) (instance ?L4 LengthMeasure) (not (equal ?T1 ?T2)) (not (equal ?TM1 ?TM2)) (holdsDuring ?TM1 (and (measure ?BTS ?T1) (measure ?M1 ?L1) (measure ?M2 ?L2))) (holdsDuring ?TM2 (and (measure ?BTS ?T2) (measure ?M1 ?L3) (measure ?M2 ?L4)))) (not (equal (DivisionFn ?L1 ?L2) (DivisionFn ?L3 ?L4)))) |
Cars.kif 4055-4087 | |
| (=> (and (instance ?BUYINGS Collection) (instance ?GMB CurrencyMeasure) (instance ?TOTAL RealNumber) (equal ?GMB (GMBFn ?BUYINGS)) (equal ?TOTAL (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Object) (exists (?BUYING) (and (member ?BUYING ?BUYINGS) (patient ?ITEM ?BUYING)))))))) (equal (ABPFn ?BUYINGS) (DivisionFn ?GMB ?TOTAL))) |
UXExperimentalTerms.kif 3442-3462 | |
| (=> (and (instance ?COLL Collection) (forall (?MEMBER) (=> (member ?MEMBER ?COLL) (instance ?MEMBER WebListing)))) (equal (DivisionFn (CardinalityFn (KappaFn ?LISTING (and (instance ?LISTING WebListing) (instance ?SITE WebSite) (instance ?ITEM Physical) (member ?LISTING ?COLL) (patient ?LISTING ?ITEM) (hostedOn ?LISTING ?SITE) (exists (?BUYING) (and (instance ?BUYING Buying) (patient ?BUYING ?ITEM) (eCommerceSite ?BUYING ?SITE)))))) (CardinalityFn ?COLL)) (BidCountFn ?COLL))) |
UXExperimentalTerms.kif 3050-3074 | |
| (=> (and (instance ?EC EngineChoke) (holdsDuring ?FSC1 (attribute ?EC DeviceOn)) (holdsDuring ?FSC2 (attribute ?EC DeviceOff)) (instance ?C EngineCylinder) (capacity ?C ?M) (instance ?FSC1 FourStrokeCompression) (instance ?FSC2 FourStrokeCompression) (eventLocated ?FSC1 ?C) (eventLocated ?FSC2 ?C) (instance ?A1 Air) (instance ?F1 Fuel) (part ?A1 ?MIX1) (part ?F1 ?MIX1) (measure ?MIX1 ?M) (instance ?A2 Air) (instance ?F2 Fuel) (part ?A2 ?MIX2) (part ?F2 ?MIX2) (measure ?MIX2 ?M) (measure ?A1 ?A1M) (measure ?A2 ?A2M) (measure ?F1 ?F1M) (measure ?F2 ?F2M)) (greaterThan (DivisionFn ?A2M ?F2M) (DivisionFn ?A1M ?F1M))) |
Cars.kif 1315-1344 | |
| (=> (and (instance ?EXPERIMENT Experimenting) (instance ?INTERVAL TimeInterval)) (equal (DivisionFn (CardinalityFn (KappaFn ?PURCHASE (and (instance ?PURCHASE Buying) (member ?PURCHASE (QualifyingPurchasesFn ?EXPERIMENT)) (during (WhenFn ?PURCHASE) ?INTERVAL)))) (CardinalityFn (KappaFn ?USER (and (member ?USER (TreatedUsersFn ?EXPERIMENT)) (instance ?ACCESSING AccessingWebPage) (during (WhenFn ?ACCESSING) ?INTERVAL) (agent ?ACCESSING ?USER))))) (PPIFn ?EXPERIMENT ?INTERVAL))) |
UXExperimentalTerms.kif 3297-3316 | |
| (=> (and (instance ?EXPERIMENT Experimenting) (instance ?INTERVAL TimeInterval)) (equal (DivisionFn (CardinalityFn (KappaFn ?PURCHASE (and (instance ?PURCHASE Buying) (member ?PURCHASE (QualifyingPurchasesFn ?EXPERIMENT))))) (CardinalityFn (KappaFn ?USER (and (member ?USER (TreatedUsersFn ?EXPERIMENT)) (instance ?ACCESSING AccessingWebPage) (agent ?ACCESSING ?USER))))) (PPSFn ?EXPERIMENT))) |
UXExperimentalTerms.kif 3258-3275 | |
| (=> (and (instance ?PAGE SearchResultsPage) (instance ?RESULTS SRPResults) (component ?RESULTS ?PAGE)) (equal (DivisionFn (CardinalityFn (KappaFn ?CLICK (and (instance ?CLICK RequestingHyperlink) (patient ?CLICK ?ELEMENT) (destination ?CLICK ?LINKEDPAGE) (instance ?ELEMENT HypertextLink) (component ?ELEMENT ?PAGE) (or (instance ?LINKEDPAGE ProductDescriptionPage) (instance ?LINKEDPAGE ViewItemPage))))) (ListLengthFn ?RESULTS)) (SRPEngagementFn ?PAGE))) |
UXExperimentalTerms.kif 3923-3941 | |
| (=> (and (instance ?QUANTITY1 Quantity) (instance ?QUANTITY2 Quantity)) (equal (LiftFn ?QUANTITY1 ?QUANTITY2) (DivisionFn (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2))) |
UXExperimentalTerms.kif 4761-4769 | |
| (=> (and (instance ?R RadiatingElectromagnetic) (carrierFrequency ?R (MeasureFn Hertz ?HZ)) (wavelength ?R (MeasureFn Meter ?L))) (equal (MeasureFn Meter ?L) (MeasureFn Meter (DivisionFn 299792458 ?HZ)))) |
ComputingBrands.kif 1546-1553 | |
| (=> (and (instance ?SELLINGS Collection) (instance ?GMV CurrencyMeasure) (instance ?TOTAL RealNumber) (equal ?GMV (GMVFn ?SELLINGS)) (equal ?TOTAL (CardinalityFn (KappaFn ?ITEM (and (instance ?ITEM Object) (exists (?SELLING) (and (member ?SELLING ?SELLINGS) (patient ?SELLING ?ITEM)))))))) (equal (ASPFn ?SELLINGS) (DivisionFn ?GMV ?TOTAL))) |
UXExperimentalTerms.kif 3485-3505 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| (equal (MeasureFn ?NUMBER AngularDegree) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn Pi 180.0)) Radian)) |
Merge.kif 7063-7065 | |
| (equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree)) |
Merge.kif 6714-6716 | |
| (equal (MeasureFn ?NUMBER Cup) (MeasureFn (DivisionFn ?NUMBER 2) Pint)) |
Merge.kif 6935-6937 | |
| (equal (MeasureFn ?NUMBER Ounce) (MeasureFn (DivisionFn ?NUMBER 8) Cup)) |
Merge.kif 6944-6946 | |
| (equal (MeasureFn ?NUMBER Pint) (MeasureFn (DivisionFn ?NUMBER 2) Quart)) |
Merge.kif 6926-6928 | |
| (equal (MeasureFn ?NUMBER Quart) (MeasureFn (DivisionFn ?NUMBER 4) UnitedStatesGallon)) |
Merge.kif 6917-6919 | |
| (forall (?NUMBER) (equal (MeasureFn ?NUMBER OunceMass) (MeasureFn (DivisionFn ?NUMBER 16) PoundMass))) |
Mid-level-ontology.kif 10977-10980 |
|
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 3.0 is open source software produced by Articulate Software and its partners