| 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 4774-4778 | |
| (documentation DivisionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (DivisionFn ?NUMBER1 ?NUMBER2) は ?NUMBER1を ?NUMBER2で除算した結果である。注１：?NUMBER1 = 1 (DivisionFn ?NUMBER1 ?NUMBER2) が ?NUMBER2 の逆数である場合がある。 注２：?NUMBER2 = 0 の場合、(DivisionFn ?NUMBER1 ?NUMBER2) は未定義である。") | japanese_format.kif 884-887 | |
| (domain DivisionFn 1 RealNumber) | Merge.kif 4770-4770 | 除法函数 的 1 数量 是 实数 的 instance |
| (domain DivisionFn 2 RealNumber) | Merge.kif 4771-4771 | 除法函数 的 2 数量 是 实数 的 instance |
| (identityElement DivisionFn 1) | Merge.kif 5325-5325 | 1 是 除法函数 的单位元 |
| (instance DivisionFn BinaryFunction) | Merge.kif 4767-4767 | 除法函数 是 二元函数 的 instance |
| (instance DivisionFn PartialValuedRelation) | Merge.kif 4769-4769 | 除法函数 是 部分值关系 的 instance |
| (range DivisionFn RealNumber) | Merge.kif 4772-4772 | 除法函数 的 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 20001-20001 | |
| (termFormat ChineseLanguage DivisionFn "除法函数") | chinese_format.kif 687-687 | |
| (termFormat ChineseTraditionalLanguage DivisionFn "部") | domainEnglishFormat.kif 20000-20000 | |
| (termFormat EnglishLanguage DivisionFn "division") | domainEnglishFormat.kif 19999-19999 | |
| (termFormat de DivisionFn "DivisionFn") | terms-de.txt 265-265 | |
| (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 19519-19530 |
|
| (=> (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 3052-3073 |
|
| (=> (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 4983-4996 | |
| (=> (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 5007-5020 | |
| (=> (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 2340-2350 | |
| (=> (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 2352-2362 | |
| (=> (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 3730-3751 |
|
| (=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5145-5156 | |
| (=> (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 540-550 | |
| (=> (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 589-599 |
| consequent |
|
|
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (BirthsPerThousandFn ?AREA ?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) ?YEAR) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA))))) (equal (DivisionFn ?BIRTHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 82-97 | 年 是 整数 year 的 instance 和 equal 地缘政治区域 和 那个 年 每一千的 births and 实数 若且唯若 equal 那个 地缘政治区域 的 population 和 1000 and 另一个 实数 和 equal 另一个 整数 and 符号串 所描述的类别 instance 的数量 和 equal 那个 另外 整数 和 那个 另外 实数 and 那个 实数 |
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (DeathsPerThousandFn ?AREA ?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) ?YEAR) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?DEATHCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 118-133 | 年 是 整数 year 的 instance 和 equal 地缘政治区域 和 那个 年 每一千里的 deaths and 实数 若且唯若 equal 那个 地缘政治区域 的 population 和 1000 and 另一个 实数 和 equal 另一个 整数 and 符号串 所描述的类别 instance 的数量 和 equal 那个 另外 整数 和 那个 另外 实数 and 那个 实数 |
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (DeathsPerThousandLiveBirthsFn ?AREA ?YEAR) ?REALNUMBER)) (and (equal ?BIRTHCOUNT (CardinalityFn (KappaFn ?BIRTH (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INFANT) (instance ?INFANT Human) (during (WhenFn ?BIRTH) ?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) ?YEAR) (equal (WhereFn ?DEATH (WhenFn ?DEATH)) ?AREA))))) (equal (DivisionFn ?INFANTDEATHCOUNT ?THOUSANDSOFBIRTHS) ?REALNUMBER))) |
People.kif 238-264 | 年 是 整数 year 的 instance 和 equal 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths and 实数 若且唯若 equal 另一个 整数 and 符号串 所描述的类别 instance 的数量 和 equal 那个 另外 整数 和 1000 and 另一个 实数 和 equal 第三 整数 and 另一个 符号串 所描述的类别 instance 的数量 和 equal 那个 第三 整数 和 那个 另外 实数 and 那个 实数 |
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (MigrantsPerThousandFn ?AREA ?YEAR) ?REALNUMBER)) (and (equal (SubtractionFn ?Y ?PY) 1) (instance ?PREVIOUSYEAR (YearFn ?PY)) (holdsDuring ?YEAR (equal (PopulationFn ?AREA) ?POPULATION)) (equal (DivisionFn ?POPULATION 1000) ?THOUSANDS) (equal ?IMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring ?PREVIOUSYEAR (not (inhabits ?PERSON ?AREA))) (holdsDuring ?YEAR (inhabits ?PERSON ?AREA)))))) (equal ?EMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring ?PREVIOUSYEAR (inhabits ?PERSON ?AREA)) (holdsDuring ?YEAR (not (inhabits ?PERSON ?AREA))))))) (equal (SubtractionFn ?IMMIGRATION ?EMMIGRATION) ?MIGRATIONCOUNT) (equal (DivisionFn ?MIGRATIONCOUNT ?THOUSANDS) ?REALNUMBER))) |
People.kif 156-187 | 年 是 整数 year 的 instance 和 equal 地缘政治区域 和 那个 年 每一千的 migrants and 实数 若且唯若 equal (那个 整数 和 另一个 整数) and 1 和 实体 是 那个 另外 整数 year 的 instance 和 equal 那个 地缘政治区域 的 population and 另一个 实数 在 那个 年 holdsDuring 和 equal 那个 另外 实数 和 1000 and 第三 实数 和 equal 第三 整数 and 符号串 所描述的类别 instance 的数量 和 equal 第四 整数 and 那个 符号串 所描述的类别 instance 的数量 和 equal (那个 第三 整数 和 那个 第四 整数) and 第四 实数 和 equal 那个 第四 实数 和 那个 第三 实数 and 那个 实数 |
| (<=> (and (instance ?YEAR (YearFn ?Y)) (equal (PopulationGrowthFn ?AREA ?YEAR) ?ADJUSTEDPERCENT)) (and (equal (SubtractionFn ?Y ?YP) 1) (instance ?PREVIOUSYEAR (YearFn ?YP)) (holdsDuring ?YEAR (equal (PopulationFn ?AREA) ?POPULATION)) (holdsDuring ?PREVIOUSYEAR (equal (PopulationFn ?AREA) ?PREVIOUSPOPULATION)) (equal (DivisionFn ?POPULATION ?PREVIOUSPOPULATION) ?PERCENT) (equal (SubtractionFn ?PERCENT 1) ?ADJUSTEDPERCENT))) |
People.kif 52-64 | 年 是 整数 year 的 instance 和 equal 地缘政治区域 和 那个 年 的 population 成长 and 实数 若且唯若 equal (那个 整数 和 那个 整数P) and 1 和 时间位置 是 那个 整数P year 的 instance 和 equal 那个 地缘政治区域 的 population and 另一个 实数 在 那个 年 holdsDuring 和 equal 那个 地缘政治区域 的 population and 第三 实数 在 那个 时间位置 holdsDuring 和 equal 那个 另外 实数 和 那个 第三 实数 and 第四 实数 和 equal (那个 第四 实数 和 1) and 那个 实数 |
| (<=> (average ?LIST1 ?AVERAGE) (exists (?LIST2 ?LASTPLACE) (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 272-293 | 实数 是 串列 的 average 若且唯若 有存在 另一个 串列 和 正整数 这样 equal 那个 另外 串列 的长度 and 那个 串列 的长度 和 equal 那个 另外 串列 的第 1 几个元素 and 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数
|
| (<=> (beliefGroupPercentInRegion ?BG ?N ?R) (exists (?G1 ?G2 ?P ?P2 ?N1 ?N2) (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 1529-1540 | 百分之 实数 在 信仰团体 的人相信 那个 信仰团体 若且唯若 有存在 群体， 另一个 群体,， ， 物理,， ， 那个 物理2,， ， 那个 实数1， and 和 那个 实数2 这样 那个 物理 是 located 在 地理区域 和 那个 物理 是 那个 信仰团体 的 member 和 那个 物理 是 那个 群体 的 member 和 那个 实数1 是 那个 群体 的 member 计数 和 那个 物理2 是 located 在 那个 地理区域 和 那个 物理2 是 那个 另外 群体 的 member 和 那个 实数2 是 那个 另外 群体 的 member 计数 和 equal 那个 实数 和 100 and 那个 实数1 和 那个 实数2 |
| (<=> (compressionRatio ?E ?R) (and (minCylinderVolume ?E (MeasureFn ?MIN ?M)) (maxCylinderVolume ?E (MeasureFn ?MAX ?M)) (equal ?R (DivisionFn ?MIN ?MAX)))) |
Cars.kif 1912-1917 | compressionRatio 发动机 and 实数 若且唯若 minCylinderVolume 那个 发动机 and 另一个 实数 测量单位 和 maxCylinderVolume 那个 发动机 and 那个 测量单位AX 那个 测量单位 和 equal 那个 实数 and 那个 另外 实数 和 那个 测量单位AX |
| (<=> (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 206-223 | equal 地缘政治区域 的 male 对母性比率 and 实数 若且唯若 equal 整数 and 符号串 所描述的类别 instance 的数量 和 equal 另一个 整数 and 另一个 符号串 所描述的类别 instance 的数量 和 equal 那个 整数 和 那个 另外 整数 and 那个 实数 |
| (<=> (ethnicityPercentInRegion ?BG ?N ?R) (exists (?G1 ?G2 ?P ?P2 ?N1 ?N2) (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 1548-1559 | 实数 percent 的人在 地理区域 是 民族群组 若且唯若 有存在 群体， 另一个 群体,， ， 物理,， ， 那个 物理2,， ， 那个 实数1， and 和 那个 实数2 这样 那个 物理 是 located 在 那个 地理区域 和 那个 物理 是 那个 民族群组 的 member 和 那个 物理 是 那个 群体 的 member 和 那个 实数1 是 那个 群体 的 member 计数 和 那个 物理2 是 located 在 那个 地理区域 和 那个 物理2 是 那个 另外 群体 的 member 和 那个 实数2 是 那个 另外 群体 的 member 计数 和 equal 那个 实数 和 100 and 那个 实数1 和 那个 实数2 |
| (<=> (languagePercentInRegion ?L ?N ?R) (exists (?G1 ?G2 ?P ?P2 ?N1 ?N2) (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 1567-1578 | 百分之 实数 的人在 地理区域 speak 语言 若且唯若 有存在 群体， 另一个 群体,， ， 有感知的主事,， ， 那个 有感知的主事2,， ， 那个 实数1， and 和 那个 实数2 这样 那个 有感知的主事 是 located 在 那个 地理区域 和 那个 有感知的主事 是 那个 群体 的 member 和 那个 语言 是 那个 有感知的主事 的 speaks 语言 和 那个 实数1 是 那个 群体 的 member 计数 和 那个 有感知的主事2 是 located 在 那个 地理区域 和 那个 有感知的主事2 是 那个 另外 群体 的 member 和 那个 实数2 是 那个 另外 群体 的 member 计数 和 equal 那个 实数 和 100 and 那个 实数1 和 那个 实数2 |
| (<=> (measure ?OBJECT (MeasureFn ?NUMBER OunceMass)) (measure ?OBJECT (MeasureFn (DivisionFn ?NUMBER 16.0) PoundMass))) |
Mid-level-ontology.kif 14665-14670 | 物理 的 measure 是 实数 OunceMass 若且唯若 那个 物理 的 measure 是 那个 实数 和 16.0 磅质量 |
| (=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5132-5143 | |
| (=> (and (equal ?A (AverageFn ?L)) (greaterThan (ListLengthFn ?L) 0)) (equal ?A (DivisionFn (ListSumFn ?L) (ListLengthFn ?L)))) |
Merge.kif 3290-3297 | |
| (=> (and (equal ?V (VarianceFn ?L)) (equal ?M (AverageFn ?L))) (equal ?V (DivisionFn (VarianceAverageFn ?M ?L) (ListLengthFn ?L)))) |
Weather.kif 2161-2170 | |
| (=> (and (gearToothCount ?G1 ?I1) (gearToothCount ?G2 ?I2) (gearRatio ?G1 ?G2 ?R)) (equal ?R (DivisionFn ?I1 ?I2))) |
engineering.kif 876-882 | |
| (=> (and (instance ?A AstronomicalBody) (approximateDiameter ?A (MeasureFn ?D ?U)) (instance ?U UnitOfLength) (instance ?P PointInSpace) (part ?P ?A)) (exists (?C) (and (equal ?C (CenterOfPlanetFn ?A)) (distance ?C ?P (MeasureFn (DivisionFn ?D 2.0) ?U))))) |
Mid-level-ontology.kif 27453-27467 |
|
| (=> (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 4142-4174 |
|
| (=> (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 ?BUYING ?ITEM)))))))) (equal (ABPFn ?BUYINGS) (DivisionFn ?GMB ?TOTAL))) |
UXExperimentalTerms.kif 3239-3259 | |
| (=> (and (instance ?COLL Collection) (forall (?MEMBER) (=> (member ?MEMBER ?COLL) (instance ?MEMBER WebListing)))) (equal (DivisionFn (CardinalityFn (exists (?LISTING ?SITE ?ITEM) (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 2845-2870 | |
| (=> (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) (instance ?U UnitOfMeasure) (measure ?A1 (MeasureFn ?A1M ?U)) (measure ?A2 (MeasureFn ?A2M ?U)) (measure ?F1 (MeasureFn ?F1M ?U)) (measure ?F2 (MeasureFn ?F2M ?U))) (greaterThan (DivisionFn ?A2M ?F2M) (DivisionFn ?A1M ?F1M))) |
Cars.kif 1314-1348 |
|
| (=> (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 3095-3114 | |
| (=> (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 3056-3073 | |
| (=> (and (instance ?H HumanAdult) (measure ?H (MeasureFn ?N Pounds))) (and (bloodVolume ?H (MeasureFn ?N2 Liter)) (equal ?N2 (DivisionFn (MultiplicationFn ?N 0.07) 2.33)))) |
Medicine.kif 5931-5940 | |
| (=> (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 3721-3739 |
|
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| (equal (MeasureFn ?NUMBER Amu) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn (DivisionFn (DivisionFn (DivisionFn 1.6605402 1000000.0) 1000000.0) 1000000.0) 1000000.0)) Gram)) |
Merge.kif 7177-7187 | equal 实数 amu and 那个 实数 和 1.6605402 和 1000000.0 和 1000000.0 和 1000000.0 和 1000000.0 公克 |
| (equal (MeasureFn ?NUMBER Angstrom) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn (DivisionFn 1.0 100000.0) 100000.0)) Meter)) |
Merge.kif 7213-7219 | equal 实数 埃 and 那个 实数 和 1.0 和 100000.0 和 100000.0 仪表 |
| (equal (MeasureFn ?NUMBER AngularDegree) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn Pi 180.0)) Radian)) |
Merge.kif 7411-7413 | equal 实数 圆周角度 and 那个 实数 和 圆周率 和 180.0 弧度 |
| (equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32.0) 1.8) FahrenheitDegree)) |
Merge.kif 7037-7039 | equal 实数 摄氏度 and (那个 实数 和 32.0) 和 1.8 华氏度 |
| (equal (MeasureFn ?NUMBER Cup) (MeasureFn (DivisionFn ?NUMBER 2) Pint)) |
Merge.kif 7283-7285 | equal 实数 杯子 and 那个 实数 和 2 品脱 |
| (equal (MeasureFn ?NUMBER ElectronVolt) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn (DivisionFn (DivisionFn 1.60217733 1000000.0) 1000000.0) 10000000.0)) Joule)) |
Merge.kif 7195-7203 | equal 实数 电子伏特 and 那个 实数 和 1.60217733 和 1000000.0 和 1000000.0 和 10000000.0 焦耳 |
| (equal (MeasureFn ?NUMBER Ounce) (MeasureFn (DivisionFn ?NUMBER 8) Cup)) |
Merge.kif 7292-7294 | equal 实数 盎司 and 那个 实数 和 8 杯子 |
| (equal (MeasureFn ?NUMBER Pint) (MeasureFn (DivisionFn ?NUMBER 2) Quart)) |
Merge.kif 7274-7276 | equal 实数 品脱 and 那个 实数 和 2 夸脱 |
| (equal (MeasureFn ?NUMBER Quart) (MeasureFn (DivisionFn ?NUMBER 4) UnitedStatesGallon)) |
Merge.kif 7265-7267 | equal 实数 夸脱 and 那个 实数 和 4 美国加仑 |
| (forall (?NUMBER) (equal (MeasureFn ?NUMBER OunceMass) (MeasureFn (DivisionFn ?NUMBER 16.0) PoundMass))) |
Mid-level-ontology.kif 14672-14675 | 对所有 实数 equal 那个 实数 OunceMass and 那个 实数 和 16.0 磅质量 |
|
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