Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - SubtractionFn
SubtractionFn

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 4410-4414
(domain SubtractionFn 1 Quantity) Merge.kif 4406-4406
(domain SubtractionFn 2 Quantity) Merge.kif 4407-4407
(identityElement SubtractionFn 0) Merge.kif 4883-4883
(instance SubtractionFn AssociativeFunction) Merge.kif 4403-4403
(instance SubtractionFn BinaryFunction) Merge.kif 4402-4402
(instance SubtractionFn TotalValuedRelation) Merge.kif 4405-4405
(range SubtractionFn Quantity) Merge.kif 4408-4408

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 55795-55795
(termFormat ChineseLanguage SubtractionFn "减法函数") chinese_format.kif 685-685
(termFormat ChineseTraditionalLanguage SubtractionFn "減法") domainEnglishFormat.kif 55794-55794
(termFormat EnglishLanguage SubtractionFn "subtraction") domainEnglishFormat.kif 55793-55793

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 3228-3235
(=>
    (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
        (instance ?DAY1
            (DayFn ?NUMBER1 ?MONTH))
        (instance ?DAY2
            (DayFn ?NUMBER2 ?MONTH))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?DAY1 ?DAY2))
Merge.kif 7939-7944
(=>
    (and
        (instance ?HOUR1
            (HourFn ?NUMBER1 ?DAY))
        (instance ?HOUR2
            (HourFn ?NUMBER2 ?DAY))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?HOUR1 ?HOUR2))
Merge.kif 7965-7970
(=>
    (and
        (instance ?MINUTE1
            (MinuteFn ?NUMBER1 ?HOUR))
        (instance ?MINUTE2
            (MinuteFn ?NUMBER2 ?HOUR))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?MINUTE1 ?MINUTE2))
Merge.kif 7992-7997
(=>
    (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 8019-8024
(=>
    (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 8084-8089
(=>
    (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 4449-4460
(<=>
    (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
(<=>
    (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
(=>
    (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 6595-6597
(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (SubtractionFn ?NUMBER 273.15) KelvinDegree))
Merge.kif 6591-6593
(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
(forall (?NUMBER)
    (equal
        (PredecessorFn ?NUMBER)
        (SubtractionFn ?NUMBER 1)))
Merge.kif 4416-4417


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