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 的负数。") 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 4731-4735
(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 4727-4727
(domain SubtractionFn 2 RealNumber) Merge.kif 4728-4728
(identityElement SubtractionFn 0) Merge.kif 5297-5297
(instance SubtractionFn BinaryFunction) Merge.kif 4724-4724
(instance SubtractionFn TotalValuedRelation) Merge.kif 4726-4726
(range SubtractionFn RealNumber) Merge.kif 4729-4729

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

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 3050-3071
(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 0))
    (equal ?R NullList))		 Merge.kif 3171-3178
(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 1))
    (equal ?R
        (ListFn
            (ListOrderFn ?L ?S))))		 Merge.kif 3180-3189
(=>
    (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 3191-3203
(=>
    (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 23946-23960
(=>
    (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 8639-8644
(=>
    (and
        (instance ?HOUR1
            (HourFn ?NUMBER1 ?DAY))
        (instance ?HOUR2
            (HourFn ?NUMBER2 ?DAY))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?HOUR1 ?HOUR2))		 Merge.kif 8665-8670
(=>
    (and
        (instance ?MINUTE1
            (MinuteFn ?NUMBER1 ?HOUR))
        (instance ?MINUTE2
            (MinuteFn ?NUMBER2 ?HOUR))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?MINUTE1 ?MINUTE2))		 Merge.kif 8692-8697
(=>
    (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 8719-8724
(=>
    (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 8784-8789
(=>
    (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 4769-4780
(<=>
    (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
(<=>
    (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
(<=>
    (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
(=>
    (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 1470-1481
(=>
    (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 14864-14873
(=>
    (and
        (instance ?QUANTITY1 Quantity)
        (instance ?QUANTITY2 Quantity))
    (equal
        (LiftFn ?QUANTITY1 ?QUANTITY2)
        (DivisionFn
            (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2)))		 UXExperimentalTerms.kif 4563-4571
(=>
    (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 17985-18010

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


(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (DivisionFn
            (SubtractionFn ?NUMBER 32.0) 1.8) FahrenheitDegree))		 Merge.kif 7013-7015
(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (SubtractionFn ?NUMBER 273.15) KelvinDegree))		 Merge.kif 7009-7011
(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 924-937
(forall (?NUMBER)
    (equal
        (PredecessorFn ?NUMBER)
        (SubtractionFn ?NUMBER 1)))		 Merge.kif 4737-4738


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 3.0 is open source software produced by Articulate Software and its partners