| 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 4509-4513 | |
| (domain SubtractionFn 1 Quantity) | Merge.kif 4505-4505 | 减法函数 的 1 数量 是 数量 的 instance |
| (domain SubtractionFn 2 Quantity) | Merge.kif 4506-4506 | 减法函数 的 2 数量 是 数量 的 instance |
| (identityElement SubtractionFn 0) | Merge.kif 4981-4981 | 0 是 减法函数 的单位元 |
| (instance SubtractionFn BinaryFunction) | Merge.kif 4502-4502 | 减法函数 是 二元函数 的 instance |
| (instance SubtractionFn TotalValuedRelation) | Merge.kif 4504-4504 | 减法函数 是 总值关系 的 instance |
| (range SubtractionFn Quantity) | Merge.kif 4507-4507 | 减法函数 的 range 是 数量 的实例 |
| 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 55747-55747 | |
| (termFormat ChineseLanguage SubtractionFn "减法函数") | chinese_format.kif 685-685 | |
| (termFormat ChineseTraditionalLanguage SubtractionFn "減法") | domainEnglishFormat.kif 55746-55746 | |
| (termFormat EnglishLanguage SubtractionFn "subtraction") | domainEnglishFormat.kif 55745-55745 |
| antecedent |
|
|
| (<=> (exists (?Income ?Tax ?TaxAmount) (and (incomeEarned ?Agent ?Income ?Activity) (amountCharged ?Tax ?TaxAmount) (causes ?Activity ?Tax) (equal ?ATIncome (SubtractionFn ?Income ?TaxAmount)))) (afterTaxIncome ?Agent ?ATIncome ?Activity)) |
FinancialOntology.kif 3229-3236 | 有存在 货币测量， 收费， and 和 那个 收费Amount 这样 人类 是 对于 %3 赚的 income 和 那个 收费Amount 是在 那个 收费 的 amount charged 和 机构性过程 causes 那个 收费 和 第三 货币测量 equal (那个 货币测量 和 那个 收费Amount) 若且唯若 从 那个 机构性过程 由 那个 人类 引申的 after tax income 是 那个 第三 货币测量 |
| (=> (and (currentAccountBalance ?Account ?Date (MeasureFn ?Balance UnitedStatesDollar)) (lessThan ?Balance 0) (equal ?Overdraft (SubtractionFn 0 ?Balance))) (overdraft ?Account (MeasureFn ?Overdraft UnitedStatesDollar) ?Date)) |
FinancialOntology.kif 732-737 | |
| (=> (and (downPayment ?Loan ?Amount) (loanForPurchase ?Loan ?Purchase) (monetaryValue ?Purchase ?Value) (equal ?Balance (SubtractionFn ?Value ?Amount))) (originalBalance ?Loan ?Balance)) |
FinancialOntology.kif 766-772 | |
| (=> (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 (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 0)) (equal ?R NullList)) |
Merge.kif 3058-3065 | |
| (=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S)))) |
Merge.kif 3067-3076 | |
| (=> (and (equal ?R (SubListFn ?S ?E ?L)) (greaterThan (SubtractionFn ?E ?S) 1)) (equal ?R (ListConcatenateFn (ListFn (ListOrderFn ?L ?S)) (SubListFn (AdditionFn 1 ?S) ?E ?L)))) |
Merge.kif 3078-3090 | |
| (=> (and (instance ?DAY1 (DayFn ?NUMBER1 ?MONTH)) (instance ?DAY2 (DayFn ?NUMBER2 ?MONTH)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?DAY1 ?DAY2)) |
Merge.kif 8040-8045 | |
| (=> (and (instance ?HOUR1 (HourFn ?NUMBER1 ?DAY)) (instance ?HOUR2 (HourFn ?NUMBER2 ?DAY)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?HOUR1 ?HOUR2)) |
Merge.kif 8066-8071 | |
| (=> (and (instance ?MINUTE1 (MinuteFn ?NUMBER1 ?HOUR)) (instance ?MINUTE2 (MinuteFn ?NUMBER2 ?HOUR)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?MINUTE1 ?MINUTE2)) |
Merge.kif 8093-8098 | |
| (=> (and (instance ?Payment Payment) (origin ?Payment (CurrencyFn ?Account)) (instance ?Account FinancialAccount) (transactionAmount ?Payment ?Amount) (currentAccountBalance ?Account (ImmediatePastFn (WhenFn ?Payment)) ?Balance1) (equal ?Balance2 (SubtractionFn ?Balance1 ?Amount))) (currentAccountBalance ?Account (ImmediateFutureFn (WhenFn ?Payment)) ?Balance2)) |
FinancialOntology.kif 408-416 | |
| (=> (and (instance ?SECOND1 (SecondFn ?NUMBER1 ?MINUTE)) (instance ?SECOND2 (SecondFn ?NUMBER2 ?MINUTE)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?SECOND1 ?SECOND2)) |
Merge.kif 8120-8125 | |
| (=> (and (instance ?Withdrawal Withdrawal) (instance ?Account FinancialAccount) (origin ?Withdrawal ?Account) (transactionAmount ?Withdrawal ?Amount) (currentAccountBalance ?Account (ImmediatePastFn (WhenFn ?Withdrawal)) ?Balance1) (equal ?Balance2 (SubtractionFn ?Balance1 ?Amount))) (currentAccountBalance ?Account (ImmediateFutureFn (FutureFn ?Withdrawal)) ?Balance2)) |
FinancialOntology.kif 449-457 | |
| (=> (and (instance ?YEAR1 Year) (instance ?YEAR2 Year) (equal (SubtractionFn ?YEAR2 ?YEAR1) (MeasureFn 1 YearDuration))) (meetsTemporally ?YEAR1 ?YEAR2)) |
Merge.kif 8185-8190 | |
| (=> (and (orientation ?OBJ ?REGION Outside) (instance ?ZONE (PerimeterAreaFn ?REGION)) (instance ?ZONE UniformPerimeterArea) (width ?ZONE (MeasureFn ?LIMIT ?UNIT)) (distance ?OBJ ?REGION (MeasureFn ?FAR ?UNIT)) (instance ?UNIT UnitOfMeasure) (greaterThan (SubtractionFn ?FAR ?LIMIT) 0)) (not (located ?OBJ ?ZONE))) |
Geography.kif 862-871 | |
| (=> (and (orientation ?OBJ ?REGION Outside) (instance ?ZONE (PerimeterAreaFn ?REGION)) (instance ?ZONE UniformPerimeterArea) (width ?ZONE (MeasureFn ?LIMIT ?UNIT)) (distance ?OBJ ?REGION (MeasureFn ?FAR ?UNIT)) (instance ?UNIT UnitOfMeasure) (lessThanOrEqualTo (SubtractionFn ?FAR ?LIMIT) 0)) (located ?OBJ ?ZONE)) |
Geography.kif 851-860 |
| consequent |
|
|
| (<=> (and (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber)) (or (and (instance ?NUMBER1 NonnegativeRealNumber) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeRealNumber) (equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1))))) |
Merge.kif 4547-4558 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0 和 那个 实数) |
| (<=> (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 | 实数 是 串列 的 average 若且唯若 有存在 另一个 串列 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 正整数
|
| (<=> (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 | 地缘政治区域 和 整数 year 每一千的 migrants equal 实数 若且唯若 (那个 整数 和 数量) equal 1 和 那个 地缘政治区域 的 population equal 另一个 数量 在 那个 整数 year holdsDuring 和 那个 另外 数量 和 1000 equal 第三 数量 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 第三 整数 equal 那个 符号串 所描述的类别 instance 的数量 和 (那个 另外 整数 和 那个 第三 整数) equal 第四 数量 和 那个 第四 数量 和 那个 第三 数量 equal 那个 实数 |
| (<=> (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 | 地缘政治区域 和 整数 year 的 population 成长 equal 实数 若且唯若 (那个 整数 和 另一个 整数) equal 1 和 那个 地缘政治区域 的 population equal 数量 在 那个 整数 year holdsDuring 和 那个 地缘政治区域 的 population equal 另一个 数量 在 那个 另外 整数 year holdsDuring 和 那个 数量 和 那个 另外 数量 equal 第三 数量 和 (那个 第三 数量 和 1) equal 那个 实数 |
| (=> (and (courseWRTMagneticNorth ?OBJ1 ?OBJ2 ?MAGDEGREE) (partlyLocated ?OBJ1 ?AREA) (partlyLocated ?OBJ2 ?AREA) (magneticVariation ?AREA ?DEGREE ?DIRECTION)) (exists (?DIFFDEGREE ?TRUEDEGREE) (and (=> (and (equal ?DIRECTION East) (equal ?DIFFDEGREE (AdditionFn ?MAGDEGREE ?DEGREE))) (courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE)) (=> (and (equal ?DIRECTION West) (equal ?DIFFDEGREE (SubtractionFn ?MAGDEGREE ?DEGREE))) (courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE))))) |
Geography.kif 3632-3649 | |
| (=> (and (instance ?QUANTITY1 Quantity) (instance ?QUANTITY2 Quantity)) (equal (LiftFn ?QUANTITY1 ?QUANTITY2) (DivisionFn (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2))) |
UXExperimentalTerms.kif 4761-4769 | |
| (=> (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 |
| statement |
|
|
| (equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree)) |
Merge.kif 6691-6693 | 实数 摄氏度 equal (那个 实数 和 32) 和 1.8 华氏度 |
| (equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree)) |
Merge.kif 6687-6689 | 实数 摄氏度 equal (那个 实数 和 273.15) 凯文度 |
| (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 | 地缘政治区域 和 年 每年的 reaching 军事男性年龄 equal 符号串 所描述的类别 instance 的数量 |
| (forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1))) |
Merge.kif 4515-4516 | 对所有 整数 (那个 整数+2) equal (那个 整数 和 1) |
|
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