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

Formal Language: 



KB Term:  Term intersection
English Word: 

  SubtractionFn

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 的负数。") Merge.kif 4882-4885
(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 4877-4881
(domain SubtractionFn 1 Quantity) Merge.kif 4874-4874 The number 1 argument of subtraction is an instance of quantity
(domain SubtractionFn 2 Quantity) Merge.kif 4875-4875 The number 2 argument of subtraction is an instance of quantity
(identityElement SubtractionFn 0) Merge.kif 5387-5387 0 is an identity element of subtraction
(instance SubtractionFn AssociativeFunction) Merge.kif 4871-4871 Subtraction is an instance of associative function
(instance SubtractionFn BinaryFunction) Merge.kif 4870-4870 Subtraction is an instance of binary function
(instance SubtractionFn TotalValuedRelation) Merge.kif 4873-4873 Subtraction is an instance of total valued relation
(range SubtractionFn Quantity) Merge.kif 4876-4876 The range of subtraction is an instance of quantity

appearance as argument number 2
-------------------------


(format ChineseLanguage SubtractionFn "(%*[-])") chinese_format.kif 684-684
(format EnglishLanguage SubtractionFn "(%*[-])") english_format.kif 426-426
(termFormat ChineseLanguage SubtractionFn "减法函数") chinese_format.kif 685-685 "减法函数" is the printable form of subtraction in ChineseLanguage
(termFormat EnglishLanguage SubtractionFn "subtraction") domainEnglishFormat.kif 9733-9733 "subtraction" is the printable form of subtraction in english language

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 3222-3229 There exist a currency measure, a chargingA fee and the chargingA feeAmount such that a human income earned the currency measure for an organizational process and the chargingA feeAmount is the amount charged in the chargingA fee and the organizational process causes the chargingA fee and a third currency measure is equal to (the currency measure and the chargingA feeAmount) if and only if the after tax income derived by the human from the organizational process is the third currency measure
(=>
    (and
        (currentAccountBalance ?Account ?Date
            (MeasureFn ?Balance UnitedStatesDollar))
        (lessThan ?Balance 0)
        (equal ?Overdraft
            (SubtractionFn 0 ?Balance)))
    (overdraft ?Account
        (MeasureFn ?Overdraft UnitedStatesDollar) ?Date))
FinancialOntology.kif 733-738
(=>
    (and
        (downPayment ?Loan ?Amount)
        (loanForPurchase ?Loan ?Purchase)
        (monetaryValue ?Purchase ?Value)
        (equal ?Balance
            (SubtractionFn ?Value ?Amount)))
    (originalBalance ?Loan ?Balance))
FinancialOntology.kif 767-773
(=>
    (and
        (instance ?DAY1
            (DayFn ?NUMBER1 ?MONTH))
        (instance ?DAY2
            (DayFn ?NUMBER2 ?MONTH))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?DAY1 ?DAY2))
Merge.kif 8726-8731
(=>
    (and
        (instance ?HOUR1
            (HourFn ?NUMBER1 ?DAY))
        (instance ?HOUR2
            (HourFn ?NUMBER2 ?DAY))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?HOUR1 ?HOUR2))
Merge.kif 8756-8761
(=>
    (and
        (instance ?MINUTE1
            (MinuteFn ?NUMBER1 ?HOUR))
        (instance ?MINUTE2
            (MinuteFn ?NUMBER2 ?HOUR))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?MINUTE1 ?MINUTE2))
Merge.kif 8788-8793
(=>
    (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 8820-8825
(=>
    (and
        (instance ?Withdrawal Withdrawal)
        (time ?Withdrawal ?TimeOfWithdrawal)
        (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 450-459
(=>
    (and
        (instance ?YEAR1 Year)
        (instance ?YEAR2 Year)
        (equal
            (SubtractionFn ?YEAR2 ?YEAR1)
            (MeasureFn 1 YearDuration)))
    (meetsTemporally ?YEAR1 ?YEAR2))
Merge.kif 8885-8890
(=>
    (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 849-858
(=>
    (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 838-847

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 4924-4935 The absolute value of a real number is equal to a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (0 and the real number)
(<=>
    (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 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
(<=>
    (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 The migrants per thousand of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and a quantity) is equal to 1 and the population of the geopolitical area is equal to another quantity holds during the year the integer and the other quantity and 1000 is equal to a third quantity and another integer is equal to the number of instances in the class described by a symbolic string and a third integer is equal to the number of instances in the class described by the symbolic string and (the other integer and the third integer) is equal to a fourth quantity and the fourth quantity and the third quantity is equal to the real number
(<=>
    (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 The population growth of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and another integer) is equal to 1 and the population of the geopolitical area is equal to a quantity holds during the year the integer and the population of the geopolitical area is equal to another quantity holds during the year the other integer and the quantity and the other quantity is equal to a third quantity and (the third quantity and 1) is equal to the real number
(=>
    (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 3619-3636
(=>
    (and
        (instance ?QUANTITY1 Quantity)
        (instance ?QUANTITY2 Quantity))
    (equal
        (LiftFn ?QUANTITY1 ?QUANTITY2)
        (DivisionFn
            (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2)))
UXExperimentalTerms.kif 4754-4762
(=>
    (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 532-541

statement
-------------------------


(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (DivisionFn
            (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree))
Merge.kif 7270-7272 A real number celsius degree(s) is equal to (the real number and 32) and 1.8 fahrenheit degree(s)
(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (SubtractionFn ?NUMBER 273.15) KelvinDegree))
Merge.kif 7266-7268 A real number celsius degree(s) is equal to (the real number and 273.15) kelvin degree(s)
(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 The reaching military age annually male of a geopolitical area and a year is equal to the number of instances in the class described by a symbolic string
(forall (?NUMBER)
    (equal
        (PredecessorFn ?NUMBER)
        (SubtractionFn ?NUMBER 1)))
Merge.kif 4887-4888 For all an integer (the integer+2) is equal to (the integer and 1)


Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree


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