| 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 4730-4734 | |
| (documentation SubtractionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (SubtractionFn ?NUMBER1 ?NUMBER2) は ?NUMBER1 と ?NUMBER2 の算術差です。すなわち、?NUMBER1 マイナス ?NUMBER2。 例外は、?NUMBER1 が 0 に等しい場合に発生し、その場合 (SubtractionFn ?NUMBER1 ?NUMBER2) は ?NUMBER2の否定である。") | japanese_format.kif 880-883 | |
| (domain SubtractionFn 1 RealNumber) | Merge.kif 4726-4726 | |
| (domain SubtractionFn 2 RealNumber) | Merge.kif 4727-4727 | |
| (identityElement SubtractionFn 0) | Merge.kif 5296-5296 | |
| (instance SubtractionFn BinaryFunction) | Merge.kif 4723-4723 | |
| (instance SubtractionFn TotalValuedRelation) | Merge.kif 4725-4725 | |
| (range SubtractionFn RealNumber) | Merge.kif 4728-4728 |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage SubtractionFn "(%*[-])") | chinese_format.kif 684-684 | |
| (format EnglishLanguage SubtractionFn "(%*[-])") | english_format.kif 686-686 | |
| (format FrenchLanguage SubtractionFn "(%*[-])") | french_format.kif 415-415 | |
| (format ItalianLanguage SubtractionFn "(%*[-]") | relations-it.txt 285-285 | |
| (format JapaneseLanguage SubtractionFn "(%*[-])") | japanese_format.kif 2132-2132 | |
| (format PortugueseLanguage SubtractionFn "(%*[-])") | portuguese_format.kif 367-367 | |
| (format cz SubtractionFn "(%*[-])") | relations-cz.txt 424-424 | |
| (format de SubtractionFn "(%*[-])") | relations-de.txt 891-891 | |
| (format hi SubtractionFn "(%*[-]") | relations-hindi.txt 322-322 | |
| (format ro SubtractionFn "(%*[-])") | relations-ro.kif 437-437 | |
| (format sv SubtractionFn "(%*[-])") | relations-sv.txt 459-459 | |
| (format tg SubtractionFn "(%*[-]") | relations-tg.txt 477-477 | |
| (termFormat ChineseLanguage SubtractionFn "减法") | domainEnglishFormat.kif 55866-55866 | |
| (termFormat ChineseLanguage SubtractionFn "减法函数") | chinese_format.kif 685-685 | |
| (termFormat ChineseTraditionalLanguage SubtractionFn "減法") | domainEnglishFormat.kif 55865-55865 | |
| (termFormat EnglishLanguage SubtractionFn "subtraction") | domainEnglishFormat.kif 55864-55864 |
| antecedent |
|
|
| (=> (and (currentAccountBalance ?Account ?Date (MeasureFn ?Balance UnitedStatesDollar)) (lessThan ?Balance 0) (equal ?Overdraft (SubtractionFn 0 ?Balance))) (overdraft ?Account (MeasureFn ?Overdraft UnitedStatesDollar) ?Date)) |
FinancialOntology.kif 783-788 | |
| (=> (and (downPayment ?Loan (MeasureFn ?Amount ?CUNIT)) (loanForPurchase ?Loan ?Purchase) (monetaryValue ?Purchase (MeasureFn ?Value ?CUNIT)) (equal ?Balance (SubtractionFn ?Value ?Amount))) (originalBalance ?Loan (MeasureFn ?Balance ?CUNIT))) |
FinancialOntology.kif 818-828 | |
| (=> (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 (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 0)) (equal ?R NullList)) |
Merge.kif 3170-3177 | |
| (=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S)))) |
Merge.kif 3179-3188 | |
| (=> (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 3190-3202 | |
| (=> (and (holdsDuring ?T1 (attribute ?F Menopausal)) (equal ?BEFORE (SubtractionFn (MeasureFn 1 YearDuration) (BeginFn ?T1))) (equal ?YBEFORE (TimeIntervalFn ?YBEFORE (BeginFn ?T1)))) (not (exists (?M) (and (instance ?M Menstruation) (experiencer ?M ?F))))) |
Mid-level-ontology.kif 23838-23852 | |
| (=> (and (incomeEarned ?Agent (MeasureFn ?Income ?CU) ?Activity) (amountCharged ?Tax (MeasureFn ?TaxAmount ?CU)) (causes ?Activity ?Tax) (equal ?ATIncome (SubtractionFn ?Income ?TaxAmount))) (afterTaxIncome ?Agent (MeasureFn ?ATIncome ?CU) ?Activity)) |
FinancialOntology.kif 3331-3341 | |
| (=> (and (instance ?DAY1 (DayFn ?NUMBER1 ?MONTH)) (instance ?DAY2 (DayFn ?NUMBER2 ?MONTH)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?DAY1 ?DAY2)) |
Merge.kif 8603-8608 | |
| (=> (and (instance ?HOUR1 (HourFn ?NUMBER1 ?DAY)) (instance ?HOUR2 (HourFn ?NUMBER2 ?DAY)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?HOUR1 ?HOUR2)) |
Merge.kif 8629-8634 | |
| (=> (and (instance ?MINUTE1 (MinuteFn ?NUMBER1 ?HOUR)) (instance ?MINUTE2 (MinuteFn ?NUMBER2 ?HOUR)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?MINUTE1 ?MINUTE2)) |
Merge.kif 8656-8661 | |
| (=> (and (instance ?Payment Payment) (origin ?Payment (CurrencyFn ?Account)) (instance ?Account FinancialAccount) (transactionAmount ?Payment (MeasureFn ?Amount ?CUNIT)) (currentAccountBalance ?Account (ImmediatePastFn (WhenFn ?Payment)) (MeasureFn ?Balance1 ?CUNIT)) (equal ?Balance2 (SubtractionFn ?Balance1 ?Amount))) (currentAccountBalance ?Account (ImmediateFutureFn (WhenFn ?Payment)) (MeasureFn ?Balance2 ?CUNIT))) |
FinancialOntology.kif 408-424 | |
| (=> (and (instance ?SECOND1 (SecondFn ?NUMBER1 ?MINUTE)) (instance ?SECOND2 (SecondFn ?NUMBER2 ?MINUTE)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?SECOND1 ?SECOND2)) |
Merge.kif 8683-8688 | |
| (=> (and (instance ?Withdrawal Withdrawal) (instance ?Account FinancialAccount) (origin ?Withdrawal ?Account) (transactionAmount ?Withdrawal (MeasureFn ?Amount ?CUNIT)) (currentAccountBalance ?Account (ImmediatePastFn (WhenFn ?Withdrawal)) (MeasureFn ?Balance1 ?CUNIT)) (equal ?Balance2 (SubtractionFn ?Balance1 ?Amount))) (currentAccountBalance ?Account (ImmediateFutureFn (FutureFn ?Withdrawal)) (MeasureFn ?Balance2 ?CUNIT))) |
FinancialOntology.kif 466-481 | |
| (=> (and (instance ?Y1 (YearFn ?N1)) (instance ?Y2 (YearFn ?N2)) (equal (SubtractionFn ?N2 ?N1) 1)) (meetsTemporally ?Y1 ?Y2)) |
Merge.kif 8748-8753 | |
| (=> (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.0)) (not (located ?OBJ ?ZONE))) |
Geography.kif 863-872 | |
| (=> (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.0)) (located ?OBJ ?ZONE)) |
Geography.kif 852-861 |
| 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.0 ?NUMBER1))))) |
Merge.kif 4768-4779 | |
| (<=> (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 182-213 | |
| (<=> (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 78-90 | |
| (<=> (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 298-319 | |
| (=> (and (equal ?VA (VarianceAverageFn ?M ?L)) (equal 1 (ListLengthFn ?L))) (equal ?VA (MultiplicationFn (SubtractionFn ?M (ListOrderFn ?L 1)) (SubtractionFn ?M (ListOrderFn ?L 1))))) |
Weather.kif 1486-1497 | |
| (=> (and (instance ?D2 (DayFn ?N2 (MonthFn ?M (YearFn ?Y)))) (temporalPart ?D1 (WeekBeforeFn ?D2)) (temporalPart ?D2 (WeekAfterFn ?D1))) (exists (?N1) (and (instance ?D1 (DayFn ?N1 (MonthFn ?M (YearFn ?Y)))) (equal ?N1 (SubtractionFn ?N2 7))))) |
Mid-level-ontology.kif 14809-14818 | |
| (=> (and (instance ?QUANTITY1 Quantity) (instance ?QUANTITY2 Quantity)) (equal (LiftFn ?QUANTITY1 ?QUANTITY2) (DivisionFn (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2))) |
UXExperimentalTerms.kif 4571-4579 | |
| (=> (and (relativeAngle ?O1 ?O2 ?N) (physicalEnd ?E1 ?O1) (physicalEnd ?E2 ?O1) (not (equal ?E1 ?E2)) (length ?O1 (MeasureFn ?N1 ?U)) (length ?O2 (MeasureFn ?N2 ?U)) (distance ?E1 ?E3 (MeasureFn ?N3 ?U)) (physicalEnd ?E3 ?O2) (physicalEnd ?E4 ?O2) (not (equal ?E3 ?E4)) (not (meetsSpatially ?E1 ?E3))) (equal ?N (ArcCosineFn (DivisionFn (SubtractionFn (SubtractionFn (MultiplicationFn ?N3 ?N3) (MultiplicationFn ?N1 ?N1)) (MultiplicationFn ?N2 ?N2)) (MultiplicationFn 2.0 (MultiplicationFn ?N1 ?N2)))))) |
Merge.kif 17876-17901 |
| statement |
|
|
| (equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32.0) 1.8) FahrenheitDegree)) |
Merge.kif 7012-7014 | |
| (equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree)) |
Merge.kif 7008-7010 | |
| (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 933-946 | |
| (forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1))) |
Merge.kif 4736-4737 |
|
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