Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 


KB Term:  Term intersection
English Word: 

Sigma KEE - SubtractionFn
SubtractionFn

appearance as argument number 1
-------------------------


(instance SubtractionFn BinaryFunction) Merge.kif 4835-4835 Subtraction is an instance of binary function
(instance SubtractionFn TotalValuedRelation) Merge.kif 4837-4837 Subtraction is an instance of total valued relation
(domain SubtractionFn 1 RealNumber) Merge.kif 4838-4838 The number 1 argument of subtraction is an instance of real number
(domain SubtractionFn 2 RealNumber) Merge.kif 4839-4839 The number 2 argument of subtraction is an instance of real number
(range SubtractionFn RealNumber) Merge.kif 4840-4840 The range of subtraction is an instance of real number
(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 4842-4846 The range of subtraction is an instance of real number
(identityElement SubtractionFn 0) Merge.kif 5419-5419 0 is an identity element of subtraction

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


(termFormat EnglishLanguage SubtractionFn "subtraction") domainEnglishFormat.kif 55849-55849
(termFormat ChineseTraditionalLanguage SubtractionFn "減法") domainEnglishFormat.kif 55850-55850
(termFormat ChineseLanguage SubtractionFn "减法") domainEnglishFormat.kif 55851-55851
(format EnglishLanguage SubtractionFn "(%*[-])") english_format.kif 686-686

antecedent
-------------------------


(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 0))
    (equal ?R NullList))		 Merge.kif 3281-3288 If equal X and the sub-list from Y to Z of W and equal (Z and Y) and 0, then equal X and null list
(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 1))
    (equal ?R
        (ListFn
            (ListOrderFn ?L ?S))))		 Merge.kif 3290-3299 If equal X and the sub-list from Y to Z of W and equal (Z and Y) and 1, then equal X and (V element of W)
(=>
    (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 3301-3313 If equal X and the sub-list from Y to Z of W and (Z and Y) is greater than 1, then equal X and the list composed of (V element of W) and the sub-list from (1 and Y) to Z of W
(=>
    (and
        (instance ?DAY1
            (DayFn ?NUMBER1 ?MONTH))
        (instance ?DAY2
            (DayFn ?NUMBER2 ?MONTH))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?DAY1 ?DAY2))		 Merge.kif 8805-8810 If X is an instance of the day Y of month Z, W is an instance of the day V of month Z, and equal (V and Y) and 1, then X meets W
(=>
    (and
        (instance ?HOUR1
            (HourFn ?NUMBER1 ?DAY))
        (instance ?HOUR2
            (HourFn ?NUMBER2 ?DAY))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?HOUR1 ?HOUR2))		 Merge.kif 8831-8836 If X is an instance of the hour Y, Z is an instance of the hour W, and equal (W and Y) and 1, then X meets Z
(=>
    (and
        (instance ?MINUTE1
            (MinuteFn ?NUMBER1 ?HOUR))
        (instance ?MINUTE2
            (MinuteFn ?NUMBER2 ?HOUR))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?MINUTE1 ?MINUTE2))		 Merge.kif 8858-8863 If X is an instance of the minute Y, Z is an instance of the minute W, and equal (W and Y) and 1, then X meets Z
(=>
    (and
        (instance ?SECOND1
            (SecondFn ?NUMBER1 ?MINUTE))
        (instance ?SECOND2
            (SecondFn ?NUMBER2 ?MINUTE))
        (equal
            (SubtractionFn ?NUMBER2 ?NUMBER1) 1))
    (meetsTemporally ?SECOND1 ?SECOND2))		 Merge.kif 8885-8890 If X is an instance of the second Y, Z is an instance of the second W, and equal (W and Y) and 1, then X meets Z
(=>
    (and
        (instance ?Y1
            (YearFn ?N1))
        (instance ?Y2
            (YearFn ?N2))
        (equal
            (SubtractionFn ?N2 ?N1) 1))
    (meetsTemporally ?Y1 ?Y2))		 Merge.kif 8950-8955 If X is an instance of the year Y, Z is an instance of the year W, and equal (W and Y) and 1, then X meets Z
(=>
    (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 26174-26188 If menopause is an attribute of X holds during Y, equal Z and (1 year duration(s) and the beginning of Y), and equal W, interval between W, and the beginning of Y, then there doesn't exist V such that V is an instance of period and X experiences V
(=>
    (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 410-426 If All of the following hold: (1) X is an instance of payment (2) X originates at the currency of Y (3) Y is an instance of financial account (4) Z W(s) is a transaction amount of X (5) Y current account balance immediately before the time of existence of X for V W(s) (6) equal U and (V and Z), then Y current account balance immediately after the time of existence of X for U W(s)
(=>
    (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 487-502 If All of the following hold: (1) X is an instance of withdrawing from an account (2) Y is an instance of financial account (3) X originates at Y (4) Z W(s) is a transaction amount of X (5) Y current account balance immediately before the time of existence of X for V W(s) (6) equal U and (V and Z), then Y current account balance immediately after after X for U W(s)
(=>
    (and
        (currentAccountBalance ?Account ?Date
            (MeasureFn ?Balance UnitedStatesDollar))
        (lessThan ?Balance 0)
        (equal ?Overdraft
            (SubtractionFn 0 ?Balance)))
    (overdraft ?Account
        (MeasureFn ?Overdraft UnitedStatesDollar) ?Date))		 FinancialOntology.kif 805-810 If X current account balance Y for Z united states dollar(s), Z is less than 0, and equal W and (0 and Z), then X is overdraft W united states dollar(s) for Y
(=>
    (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 840-850 If X Y(s) is a down payment of Z, W is a loan for purchase of Z, value of W is V Y(s), and equal U and (V and X), then U Y(s) is an original balance of Z
(=>
    (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 3388-3398 If X is income earned Y Z(s) for W, V Z(s) is the amount charged in U, W causes U, and equal T and (Y and V), then the after tax income derived by X from W is T Z(s)
(=>
    (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 2310-2319 If All of the following hold: (1) X is outside of to Y (2) Z is an instance of the perimeter area of Y (3) Z is an instance of uniform perimeter area (4) the width of Z is W V(s) (5) the distance between X and Y is U V(s) (6) V is an instance of unit of measure (7) (U and W) is less than or equal to 0.0, then X is located at Z
(=>
    (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 2321-2330 If All of the following hold: (1) X is outside of to Y (2) Z is an instance of the perimeter area of Y (3) Z is an instance of uniform perimeter area (4) the width of Z is W V(s) (5) the distance between X and Y is U V(s) (6) V is an instance of unit of measure (7) (U and W) is greater than 0.0, then X is not located at Z
(=>
    (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 2997-3018 If All of the following hold: (1) equal X and the reverse of Y (2) equal Z and the length of Y (3) Z is greater than 1 (4) W is greater than 0 (5) W is less than Z (6) equal V and the ceiling of (Z and 1) and 2 (7) equal U and ((V and W) and V) (8) equal T and the sub-string of Y from W to (1 and W), then equal T and the sub-string of X from U to (1 and U)
(=>
    (and
        (duration ?T
            (MeasureFn ?P MonthDuration))
        (greaterThanOrEqualTo ?P 5)
        (holdsDuring ?T
            (and
                (equal ?D
                    (SubtractionFn ?S ?L))
                (equal
                    (MeasureFn ?S CelsiusDegree)
                    (ThreeMonthsRunningMeanSSTFn Nino3Point4 ?M ?Y))
                (equal
                    (MeasureFn ?L CelsiusDegree)
                    (ThirtyYearAverageSSTForMonthFn Nino3Point4 ?M ?Y))
                (greaterThan ?D 0.5))))
    (holdsDuring ?T
        (exists (?EL ?A)
            (and
                (instance ?EL ElNinoPhase)
                (instance ?A GeographicArea)
                (eventLocated ?EL ?A)))))		 Weather.kif 528-549 If duration of X is Y month duration(s), Y is greater than or equal to 5, and equal Z and (W and V) and equal W celsius degree(s) and ThreeMonthsRunningMeanSSTFn for month U year T in region Nino 3.4 and equal V celsius degree(s) and ThirtyYearAverageSSTForMonthFn for month U in year T of region Nino 3.4 and Z is greater than 0.5 holds during X, then there exist S, R such that S is an instance of El Nino phase, R is an instance of geographic area, and S is located at R holds during X
(=>
    (and
        (duration ?T
            (MeasureFn ?P MonthDuration))
        (greaterThanOrEqualTo ?P 5)
        (holdsDuring ?T
            (and
                (equal ?D
                    (SubtractionFn ?S ?L))
                (equal
                    (MeasureFn ?S CelsiusDegree)
                    (ThreeMonthsRunningMeanSSTFn Nino3Point4 ?M ?Y))
                (equal
                    (MeasureFn ?L CelsiusDegree)
                    (ThirtyYearAverageSSTForMonthFn Nino3Point4 ?M ?Y))
                (lessThan ?D -0.5))))
    (holdsDuring ?T
        (exists (?LA ?A)
            (and
                (instance ?LA LaNinaPhase)
                (instance ?A GeographicArea)
                (eventLocated ?LA ?A)))))		 Weather.kif 563-584 If duration of X is Y month duration(s), Y is greater than or equal to 5, and equal Z and (W and V) and equal W celsius degree(s) and ThreeMonthsRunningMeanSSTFn for month U year T in region Nino 3.4 and equal V celsius degree(s) and ThirtyYearAverageSSTForMonthFn for month U in year T of region Nino 3.4 and Z is less than -0.5 holds during X, then there exist S, R such that S is an instance of La Nina phase, R is an instance of geographic area, and S is located at R holds during X
(=>
    (holdsDuring ?T
        (and
            (equal ?D
                (SubtractionFn ?S ?L))
            (equal
                (MeasureFn ?S CelsiusDegree)
                (ThreeMonthsRunningMeanSSTFn Nino3Point4 ?M ?Y))
            (equal
                (MeasureFn ?L CelsiusDegree)
                (ThirtyYearAverageSSTForMonthFn Nino3Point4 ?M ?Y))
            (greaterThanOrEqualTo ?D -0.5)
            (lessThanOrEqualTo ?D 0.5)))
    (holdsDuring ?T
        (exists (?N ?A)
            (and
                (instance ?N ENSONeutralPhase)
                (instance ?A GeographicArea)
                (eventLocated ?N ?A)))))		 Weather.kif 592-610 If equal X and (Y and Z) and equal Y celsius degree(s) and ThreeMonthsRunningMeanSSTFn for month W year V in region Nino 3.4 and equal Z celsius degree(s) and ThirtyYearAverageSSTForMonthFn for month W in year V of region Nino 3.4 and X is greater than or equal to -0.5 and X is less than or equal to 0.5 holds during U, then there exist T, S such that T is an instance of Enso neutral phase, S is an instance of geographic area, and T is located at S holds during U
(=>
    (and
        (equal ?TEMP
            (ThirtyYearAverageSSTForMonthFn ?W ?M ?Y))
        (instance ?Y
            (YearFn ?I))
        (equal ?YEAR
            (SubtractionFn ?I ?N))
        (greaterThanOrEqualTo ?N 0)
        (lessThan ?N 30)
        (instance ?U UnitOfTemperature)
        (equal
            (MeasureFn ?X ?U)
            (MeanMonthSSTFn ?W ?M
                (YearFn ?YEAR)))
        (inList ?X ?L))
    (equal ?TEMP
        (MeasureFn
            (AverageFn ?L) ?U)))		 Weather.kif 822-839 If All of the following hold: (1) equal X and ThirtyYearAverageSSTForMonthFn for month Y in year Z of region W (2) Z is an instance of the year V (3) equal U and (V and T) (4) T is greater than or equal to 0 (5) T is less than 30 (6) S is an instance of unit of temperature (7) equal R S(s) and MeanMonthSSTFn for Y in region W (8) R is a member of Q, then equal X and the average of the numbers in Q S(s)
(=>
    (and
        (instance ?S Squall)
        (eventLocated ?S ?R)
        (instance ?R GeographicArea)
        (holdsDuring
            (WhenFn ?S)
            (surfaceWindSpeed ?R
                (MeasureFn ?TOP MilesPerHour)))
        (earlier ?T
            (WhenFn ?S))
        (holdsDuring ?T
            (surfaceWindSpeed ?R
                (MeasureFn ?BASE MilesPerHour)))
        (equal ?DIFF
            (SubtractionFn ?TOP ?BASE)))
    (and
        (greaterThanOrEqualTo ?TOP 25)
        (greaterThanOrEqualTo ?DIFF 18)))		 Weather.kif 2265-2282 If All of the following hold: (1) X is an instance of squall (2) X is located at Y (3) Y is an instance of geographic area (4) Z miles per hour(s) is a surface wind speed of Y holds during the time of existence of X (5) W happens earlier than the time of existence of X (6) V miles per hour(s) is a surface wind speed of Y holds during W (7) equal U and (Z and V), then Z is greater than or equal to 25 and U is greater than or equal to 18
(=>
    (and
        (instance ?G WindGust)
        (eventLocated ?G ?R)
        (instance ?R GeographicArea)
        (equal
            (ThreeSecondGustSpeedFn ?R
                (WhenFn ?G))
            (MeasureFn ?TOP MilesPerHour))
        (earlier ?T
            (WhenFn ?G))
        (holdsDuring ?T
            (surfaceWindSpeed ?R
                (MeasureFn ?BASE MilesPerHour)))
        (equal ?DIFF
            (SubtractionFn ?TOP ?BASE)))
    (and
        (greaterThanOrEqualTo ?TOP 18)
        (greaterThanOrEqualTo ?DIFF 10)))		 Weather.kif 2313-2329 If All of the following hold: (1) X is an instance of wind gust (2) X is located at Y (3) Y is an instance of geographic area (4) equal ThreeSecondSpeedGustFn ending at the time of existence of X in Y and Z miles per hour(s) (5) W happens earlier than the time of existence of X (6) V miles per hour(s) is a surface wind speed of Y holds during W (7) equal U and (Z and V), then Z is greater than or equal to 18 and U is greater than or equal to 10
(=>
    (and
        (instance ?G WindGust)
        (eventLocated ?G ?R)
        (instance ?R GeographicArea)
        (equal
            (ThreeSecondGustSpeedFn ?R
                (WhenFn ?G))
            (MeasureFn ?TOP MilesPerHour))
        (earlier
            (WhenFn ?G) ?T)
        (holdsDuring ?T
            (surfaceWindSpeed ?R
                (MeasureFn ?BASE MilesPerHour)))
        (equal ?DIFF
            (SubtractionFn ?TOP ?BASE)))
    (greaterThanOrEqualTo ?DIFF 10))		 Weather.kif 2331-2345 If All of the following hold: (1) X is an instance of wind gust (2) X is located at Y (3) Y is an instance of geographic area (4) equal ThreeSecondSpeedGustFn ending at the time of existence of X in Y and Z miles per hour(s) (5) the time of existence of X happens earlier than W (6) V miles per hour(s) is a surface wind speed of Y holds during W (7) equal U and (Z and V), then U is greater than or equal to 10
(=>
    (and
        (instance ?G WeakGust)
        (eventLocated ?G ?R)
        (instance ?R GeographicArea)
        (equal
            (ThreeSecondGustSpeedFn ?R
                (WhenFn ?G))
            (MeasureFn ?TOP MilesPerHour))
        (earlier ?T
            (WhenFn ?G))
        (holdsDuring ?T
            (surfaceWindSpeed ?R
                (MeasureFn ?BASE MilesPerHour)))
        (equal ?DIFF
            (SubtractionFn ?TOP ?BASE)))
    (and
        (greaterThanOrEqualTo ?DIFF 12)
        (lessThanOrEqualTo ?DIFF 17)))		 Weather.kif 2352-2368 If All of the following hold: (1) X is an instance of weak gust (2) X is located at Y (3) Y is an instance of geographic area (4) equal ThreeSecondSpeedGustFn ending at the time of existence of X in Y and Z miles per hour(s) (5) W happens earlier than the time of existence of X (6) V miles per hour(s) is a surface wind speed of Y holds during W (7) equal U and (Z and V), then U is greater than or equal to 12 and U is less than or equal to 17

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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 4880-4891 equal the absolute value of X and Y and X is an instance of real number and Y is an instance of real number if and only if X is an instance of nonnegative real number and equal X and Y or X is an instance of negative real number and equal Y and (0.0 and X)
(=>
    (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 18247-18272 If All of the following hold: (1) the relative angle between X and Y is Z (2) one end of X is W (3) one end of X is V (4) equal W and V (5) the length of X is U T(s) (6) the length of Y is S T(s) (7) the distance between W and R is Q T(s) (8) one end of Y is R (9) one end of Y is P (10) equal R and P (11) W doesn't meet R, then equal Z and the arccosine of ((Q and Q and U and U) and S and S) and 2.0 and U and S
(=>
    (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 16444-16453 If X is an instance of the day Y of month the month Z, W is a part of week before fn X, and X is a part of week after fn W, then there exists V such that W is an instance of the day V of month the month Z and equal V and (Y and 7)
(=>
    (and
        (resourceConsumption ?PROC ?QUANT)
        (instance ?QUANT ConstantQuantity)
        (resource ?PROC ?RES)
        (holdsDuring
            (BeginFn
                (WhenFn ?PROC))
            (measure ?RES
                (MeasureFn ?X ?U)))
        (holdsDuring
            (EndFn
                (WhenFn ?PROC))
            (measure ?RES
                (MeasureFn ?Y ?U))))
    (equal ?QUANT
        (MeasureFn
            (SubtractionFn ?X ?Y) ?U)))		 Mid-level-ontology.kif 18901-18917 If X amount as resource for the Process Y, X is an instance of constant quantity, Z is a resource for Y, the measure of Z is W V(s) holds during the beginning of the time of existence of Y, and the measure of Z is U V(s) holds during the end of the time of existence of Y, then equal X and (W and U) V(s)
(=>
    (and
        (resourceConsumption ?PROC ?QUANT)
        (instance ?QUANT FunctionQuantity)
        (resource ?PROC ?RES)
        (equal ?QUANT
            (PerFn
                (MeasureFn ?Q ?U)
                (MeasureFn ?DC ?DU)))
        (duration
            (WhenFn ?PROC)
            (MeasureFn ?T ?DU))
        (holdsDuring
            (BeginFn
                (WhenFn ?PROC))
            (measure ?RES
                (MeasureFn ?X ?U)))
        (holdsDuring
            (EndFn
                (WhenFn ?PROC))
            (measure ?RES
                (MeasureFn ?Y ?U))))
    (equal ?Y
        (MeasureFn
            (SubtractionFn ?X
                (MultiplicationFn ?T
                    (DivisionFn ?Q ?DC))) ?U)))		 Mid-level-ontology.kif 18957-18983 If All of the following hold: (1) X amount as resource for the Process Y (2) X is an instance of function quantity (3) Z is a resource for Y (4) equal X and the per of W V(s) and U T(s) (5) duration of the time of existence of Y is S T(s) (6) the measure of Z is R V(s) holds during the beginning of the time of existence of Y (7) the measure of Z is Q V(s) holds during the end of the time of existence of Y, then equal Q and (R and S and W and U) V(s)
(=>
    (and
        (instance ?AREA GeographicArea)
        (objectGeographicCoordinates ?AREA ?LAT ?LONG)
        (equal
            (MeasureFn ?DEG AngularDegree)
            (MagneticDeclinationFn ?LAT ?LONG)))
    (exists (?TN)
        (and
            (headingWRTTrueNorth ?AREA
                (MeasureFn ?TN AngularDegree))
            (headingWRTMagneticNorth ?AREA
                (MeasureFn
                    (SubtractionFn ?TN ?DEG) AngularDegree)))))		 Geography.kif 5236-5248 If X is an instance of geographic area, X is object geographic coordinates Y for Z, and equal W angular degree(s) and Location on Earth at Latitude Y and Longitude Z has a magnetic declination of PlaneAngleMeasure. (+) denotes easterly declination, (-) denotes westerly declination. zero value means at the agonic line., then there exists V such that V angular degree(s) is a headingWRT true north of X and (V and W) angular degree(s) is a headingWRT magnetic north of X
(<=>
    (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 X is an instance of the year Y and equal the population growth of Z and X and W if and only if equal (Y and V) and 1 and U is an instance of the year V and equal the population of Z and T holds during X and equal the population of Z and S holds during U and equal T and S and R and equal (R and 1) and W
(=>
    (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 190-221 If X is an instance of the year Y and equal the migrants per thousand of Z, X, and W, then All of the following hold: (1) equal (Y and V) and 1 (2) U is an instance of the year V (3) equal the population of Z and T holds during X (4) equal T, 1000, and S (5) equal R and the number of instances in the class described by Q (6) equal P and the number of instances in the class described by Q (7) equal (R and P) and O (8) equal O, S, and W
(=>
    (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 306-327 If X is an average of Y, then there exist Z and W such that equal length of Z and length of Y and equal 1th element of Z and 1th element of Y and V V is a member of Zthere exist U, T,, , S and R such that U is greater than 1 and U is less than or equal to length of Z and equal Q element of Z and U and S is a member of Y and equal U and P element of Y and R is a member of Z and equal T and (U and 1) and equal T and O element of Z and equal V and (S and R) and equal W and length of Z and equal X and N element of Z and W
(=>
    (and
        (instance ?QUANTITY1 Quantity)
        (instance ?QUANTITY2 Quantity))
    (equal
        (LiftFn ?QUANTITY1 ?QUANTITY2)
        (DivisionFn
            (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2)))		 UXExperimentalTerms.kif 4560-4568 If X is an instance of quantity and Y is an instance of quantity, then equal the financial improvement percentage of X over Y and (X and Y) and Y
(=>
    (and
        (previousMonthYear ?M1 ?Y1 ?M2 ?Y2)
        (instance ?Y2
            (YearFn ?I))
        (equal ?M2
            (MonthFn January
                (YearFn ?I))))
    (and
        (equal ?M1 December)
        (instance ?Y1
            (YearFn
                (SubtractionFn ?I 1)))))		 Weather.kif 762-773 If the previous month of X in year Y is Z W, Y is an instance of the year V, and equal X and the month January, then equal Z and December and W is an instance of the year (V and 1)
(=>
    (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 2796-2807 If equal X and VarianceAverageFn of Y with the mean of Z and equal 1 and length of Y, then equal X and (Z and 1th element of Y) and (Z and 1th element of Y)
(=>
    (equal
        (MeasureFn ?Z Millimeter)
        (DiffPupilSizeFn ?P))
    (exists (?L ?R ?X ?Y)
        (and
            (member ?L ?P)
            (member ?R ?P)
            (approximateDiameter ?L
                (MeasureFn ?X Millimeter))
            (approximateDiameter ?R
                (MeasureFn ?Y Millimeter))
            (equal ?Z
                (SubtractionFn ?X ?Y)))))		 emotion.kif 1120-1131 If equal X millimeter(s) and The difference in size of Y is, then there exist Z, W,, , V and U such that Z is a member of Y and W is a member of Y and the approximate diameter of Z is V millimeter(s) and the approximate diameter of W is U millimeter(s) and equal X and (V and U)

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


(forall (?NUMBER)
    (equal
        (PredecessorFn ?NUMBER)
        (SubtractionFn ?NUMBER 1)))		 Merge.kif 4848-4849 For all Integer X: equal (X+2) and (X and 1)
(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (SubtractionFn ?NUMBER 273.15) KelvinDegree))		 Merge.kif 7127-7129 equal X celsius degree(s) and (X and 273.15) kelvin degree(s)
(equal
    (MeasureFn ?NUMBER CelsiusDegree)
    (MeasureFn
        (DivisionFn
            (SubtractionFn ?NUMBER 32.0) 1.8) FahrenheitDegree))		 Merge.kif 7131-7133 equal X celsius degree(s) and (X and 32.0) and 1.8 fahrenheit 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 1197-1210 equal the reaching military age annually male of X, Y, and the number of instances in the class described by Z


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.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners