TreeView Knowledge Base Browser

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 4783-4787
(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 4779-4779	The number 1 argument of subtraction is an instance of real number
(domain SubtractionFn 2 RealNumber)	Merge.kif 4780-4780	The number 2 argument of subtraction is an instance of real number
(identityElement SubtractionFn 0)	Merge.kif 5349-5349	0 is an identity element of subtraction
(instance SubtractionFn BinaryFunction)	Merge.kif 4776-4776	Subtraction is an instance of binary function
(instance SubtractionFn TotalValuedRelation)	Merge.kif 4778-4778	Subtraction is an instance of total valued relation
(range SubtractionFn RealNumber)	Merge.kif 4781-4781	The range of subtraction is an instance of real number

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

antecedent

(=> (and (currentAccountBalance ?Account ?Date (MeasureFn ?Balance UnitedStatesDollar)) (lessThan ?Balance 0) (equal ?Overdraft (SubtractionFn 0 ?Balance))) (overdraft ?Account (MeasureFn ?Overdraft UnitedStatesDollar) ?Date))	FinancialOntology.kif 785-790	If a financial account current account balance a day for a real number united states dollar(s) and the real number is less than 0 and equal an integer and (0 and the real number), then the financial account is overdraft the integer united states dollar(s) for the day
(=> (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 820-830	If a real number an unit of measure(s) is a down payment of a loan and an object is a loan for purchase of the loan and value of the object is another real number the unit of measure(s) and equal an integer and (the other real number and the real number), then the integer the unit of measure(s) is an original balance of the loan
(=> (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 544-565	If duration of a time interval is a real number month duration(s) and the real number is greater than or equal to 5 and equal an entity and (another entity and a third entity) and equal the other entity celsius degree(s) and ThreeMonthsRunningMeanSSTFn for month a fourth entity year a fifth entity in region Nino 3.4 and equal the third entity celsius degree(s) and ThirtyYearAverageSSTForMonthFn for month the fourth entity in year the fifth entity of region Nino 3.4 and the entity is greater than 0.5 holds during the time interval, then there exist a sixth entity and a seventh entity such that the sixth entity is an instance of El Nino phase and the seventh entity is an instance of geographic area and the sixth entity is located at the seventh entity holds during the time interval
(=> (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 579-600	If duration of a time interval is a real number month duration(s) and the real number is greater than or equal to 5 and equal an entity and (another entity and a third entity) and equal the other entity celsius degree(s) and ThreeMonthsRunningMeanSSTFn for month a fourth entity year a fifth entity in region Nino 3.4 and equal the third entity celsius degree(s) and ThirtyYearAverageSSTForMonthFn for month the fourth entity in year the fifth entity of region Nino 3.4 and the entity is less than -0.5 holds during the time interval, then there exist the third entityA and a seventh entity such that the third entityA is an instance of La Nina phase and the seventh entity is an instance of geographic area and the third entityA is located at the seventh entity holds during the time interval
(=> (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 3052-3073	If equal a symbolic string and the reverse of another symbolic string and equal an integer and the length of the other symbolic string and the integer is greater than 1 and a nonnegative integer is greater than 0 and the nonnegative integer is less than the integer and equal another integer and the ceiling of (the integer and 1) and 2 and equal the nonnegative integerEW and ((the other integer and the nonnegative integer) and the other integer) and equal a third symbolic string and the sub-string of the other symbolic string from the nonnegative integer to (1 and the nonnegative integer), then equal the third symbolic string and the sub-string of the symbolic string from the nonnegative integerEW to (1 and the nonnegative integerEW)
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 0)) (equal ?R NullList))	Merge.kif 3208-3215	If equal a list and the sub-list from an integer to another integer of another list and equal (the other integer and the integer) and 0, then equal the list and null list
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S))))	Merge.kif 3217-3226	If equal a list and the sub-list from a positive integer to an integer of another list and equal (the integer and the positive integer) and 1, then equal the list and (the positive integerth element of the other list)
(=> (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 3228-3240	If equal a list and the sub-list from a positive integer to an integer of another list and (the integer and the positive integer) is greater than 1, then equal the list and the list composed of (the positive integerth element of the other list) and the sub-list from (1 and the positive integer) to the integer of the other list
(=> (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 ?YEAR)) (inList ?X ?L)) (equal ?TEMP (MeasureFn (AverageFn ?L) ?U)))	Weather.kif 838-855	If equal a temperature measure and ThirtyYearAverageSSTForMonthFn for month a kind of month in year a year of region a water area and the year is an instance of the year an integer and equal the yearEAR and (the integer and a real number) and the real number is greater than or equal to 0 and the real number is less than 30 and an unit of measure is an instance of unit of temperature and equal another real number the unit of measure(s) and MeanMonthSSTFn for a kind of month in region the water area and the other real number is a member of a list, then equal the temperature measure and the average of the numbers in the list the unit of measure(s)
(=> (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 25526-25540	If menopause is an attribute of an agent holds during a time interval and equal an integer and (1 year duration(s) and the beginning of the time interval) and equal another time interval and interval between the other time interval and the beginning of the time interval, then there doesn't exist a process such that the process is an instance of menstruation and the agent experiences the process
(=> (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 3348-3358	If a human is income earned a real number an unit of measure(s) for an organizational process and another real number the unit of measure(s) is the amount charged in a charging a fee and the organizational process causes the charging a fee and equal an integer and (the real number and the other real number), then the after tax income derived by the human from the organizational process is the integer the unit of measure(s)
(=> (and (instance ?DAY1 (DayFn ?NUMBER1 ?MONTH)) (instance ?DAY2 (DayFn ?NUMBER2 ?MONTH)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?DAY1 ?DAY2))	Merge.kif 8738-8743	If a time interval is an instance of the day a positive integer of month a kind of month and another time interval is an instance of the day another positive integer of month a kind of month and equal (the other positive integer and the positive integer) and 1, then the time interval meets the other time interval
(=> (and (instance ?G StrongGust) (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 (greaterThan ?DIFF 17) (lessThanOrEqualTo ?DIFF 29)))	Weather.kif 2390-2406	If a process is an instance of strong gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal an integer and (the real number and the other real number), then the integer is greater than 17 and the integer is less than or equal to 29
(=> (and (instance ?G ViolentGust) (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))) (greaterThan ?DIFF 29))	Weather.kif 2413-2427	If a process is an instance of violent gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal an integer and (the real number and the other real number), then the integer is greater than 29
(=> (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 2367-2383	If a process is an instance of weak gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal an integer and (the real number and the other real number), then the integer is greater than or equal to 12 and the integer is less than or equal to 17
(=> (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 2346-2360	If a process is an instance of wind gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and the time of existence of the process happens earlier than a time interval and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal an integer and (the real number and the other real number), then the integer 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 ?T (WhenFn ?G)) (holdsDuring ?T (surfaceWindSpeed ?R (MeasureFn ?BASE MilesPerHour))) (equal ?DIFF (SubtractionFn ?TOP ?BASE))) (and (greaterThanOrEqualTo ?TOP 18) (greaterThanOrEqualTo ?DIFF 10)))	Weather.kif 2328-2344	If a process is an instance of wind gust and the process is located at a geographic area and the geographic area is an instance of geographic area and equal ThreeSecondSpeedGustFn ending at the time of existence of the process in the geographic area and a real number miles per hour(s) and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the geographic area holds during the time interval and equal an integer and (the real number and the other real number), then the real number is greater than or equal to 18 and the integer is greater than or equal to 10
(=> (and (instance ?HOUR1 (HourFn ?NUMBER1 ?DAY)) (instance ?HOUR2 (HourFn ?NUMBER2 ?DAY)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?HOUR1 ?HOUR2))	Merge.kif 8764-8769	If a time interval is an instance of the hour a nonnegative integer and another time interval is an instance of the hour another nonnegative integer and equal (the other nonnegative integer and the nonnegative integer) and 1, then the time interval meets the other time interval
(=> (and (instance ?MINUTE1 (MinuteFn ?NUMBER1 ?HOUR)) (instance ?MINUTE2 (MinuteFn ?NUMBER2 ?HOUR)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?MINUTE1 ?MINUTE2))	Merge.kif 8791-8796	If a time interval is an instance of the minute a nonnegative integer and another time interval is an instance of the minute another nonnegative integer and equal (the other nonnegative integer and the nonnegative integer) and 1, then the time interval meets the other time interval
(=> (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 a financial transaction is an instance of payment and the financial transaction originates at the currency of a financial account and the financial account is an instance of financial account and a real number an unit of measure(s) is a transaction amount of the financial transaction and the financial account current account balance immediately before the time of existence of the financial transaction for another real number the unit of measure(s) and equal an integer and (the other real number and the real number), then the financial account current account balance immediately after the time of existence of the financial transaction for the integer the unit of measure(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 2280-2297	If a process is an instance of squall and the process is located at an object and the object is an instance of geographic area and a real number miles per hour(s) is a surface wind speed of the object holds during the time of existence of the process and a time interval happens earlier than the time of existence of the process and another real number miles per hour(s) is a surface wind speed of the object holds during the time interval and equal an integer and (the real number and the other real number), then the real number is greater than or equal to 25 and the integer is greater than or equal to 18
(=> (and (instance ?SECOND1 (SecondFn ?NUMBER1 ?MINUTE)) (instance ?SECOND2 (SecondFn ?NUMBER2 ?MINUTE)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?SECOND1 ?SECOND2))	Merge.kif 8818-8823	If a time interval is an instance of the second a positive integer and another time interval is an instance of the second another positive integer and equal (the other positive integer and the positive integer) and 1, then the time interval meets the other time interval
(=> (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 468-483	If a financial transaction is an instance of withdrawing from an account and a financial account is an instance of financial account and the financial transaction originates at the financial account and a real number an unit of measure(s) is a transaction amount of the financial transaction and the financial account current account balance immediately before the time of existence of the financial transaction for another real number the unit of measure(s) and equal an integer and (the other real number and the real number), then the financial account current account balance immediately after after the financial transaction for the integer the unit of measure(s)
(=> (and (instance ?Y1 (YearFn ?N1)) (instance ?Y2 (YearFn ?N2)) (equal (SubtractionFn ?N2 ?N1) 1)) (meetsTemporally ?Y1 ?Y2))	Merge.kif 8883-8888	If a time interval is an instance of the year an integer and another time interval is an instance of the year another integer and equal (the other integer and the integer) and 1, then the time interval meets the other time interval
(=> (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 2338-2347	If an object is outside to a region and another object is an instance of the perimeter area of the region and the other object is an instance of uniform perimeter area and the width of the other object is a real number an unit of measure(s) and the distance between the object and the region is another real number the unit of measure(s) and the unit of measure is an instance of unit of measure and (the other real number and the real number) is greater than 0.0, then the object is not located at the other object

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 4821-4832	equal the absolute value of a real number and an integer and the real number is an instance of real number and the integer is an instance of real number if and only if the real number is an instance of nonnegative real number and equal the real number and the integer or the real number is an instance of negative real number and equal the integer and (0.0 and the real number)
(<=> (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	A year is an instance of the year an integer and equal the migrants per thousand of a geopolitical area and the year and a real number if and only if equal (the integer and another integer) and 1 and an entity is an instance of the year the other integer and equal the population of the geopolitical area and another real number holds during the year and equal the other real number and 1000 and a third real number and equal a third integer and the number of instances in the class described by a symbolic string and equal a fourth integer and the number of instances in the class described by the symbolic string and equal (the third integer and the fourth integer) and a fifth integer and equal the fifth integer and the third real number and the real number
(<=> (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	A year is an instance of the year an integer and equal the population growth of a geopolitical area and the year and another integer if and only if equal (the integer and the integerP) and 1 and a time position is an instance of the year the integerP and equal the population of the geopolitical area and a real number holds during the year and equal the population of the geopolitical area and another real number holds during the time position and equal the real number and the other real number and a third real number and equal (the third real number and 1) and the other integer
(<=> (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	A real number is an average of a list if and only if there exist another list and a positive integer such that equal length of the other list and length of the list and equal 1th element of the other list and 1th element of the list and for all another positive integer if the other positive integer is a member of the other list, then there exist an integer, the integerMINUSONE,, , a third positive integer and a fourth positive integer such that the integer is greater than 1 and the integer is less than or equal to length of the other list and equal the other positive integerth element of the other list and the integer and the third positive integer is a member of the list and equal the integer and the third positive integerth element of the list and the fourth positive integer is a member of the other list and equal the integerMINUSONE and (the integer and 1) and equal the integerMINUSONE and the fourth positive integerth element of the other list and equal the other positive integer and (the third positive integer and the fourth positive integer) and equal the positive integer and length of the other list and equal the real number and the positive integerth element of the other list and the positive integer
(=> (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 2811-2822	If equal an integer and VarianceAverageFn of a list with the mean of a real number and equal 1 and length of the list, then equal the integer and (the real number and 1th element of the list) and (the real number and 1th element of the list)
(=> (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 5278-5290	If an object is an instance of geographic area and the object is object geographic coordinates a latitude for a longitude and equal a real number angular degree(s) and Location on Earth at Latitude the latitude and Longitude the longitude has a magnetic declination of PlaneAngleMeasure. (+) denotes easterly declination, (-) denotes westerly declination. zero value means at the agonic line., then there exists another real number such that the other real number angular degree(s) is a headingWRT true north of the object and (the other real number and the real number) angular degree(s) is a headingWRT magnetic north of the object
(=> (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 16199-16208	If a time position is an instance of the day a positive integer of month the month a kind of month and another time position is a part of week before fn the time position and the time position is a part of week after fn the other time position, then there exists another positive integer such that the other time position is an instance of the day the other positive integer of month the month a kind of month and equal the other positive integer and (the positive integer and 7)
(=> (and (instance ?QUANTITY1 Quantity) (instance ?QUANTITY2 Quantity)) (equal (LiftFn ?QUANTITY1 ?QUANTITY2) (DivisionFn (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2)))	UXExperimentalTerms.kif 4562-4570	If a real number is an instance of quantity and another real number is an instance of quantity, then equal the financial improvement percentage of the real number over the other real number and (the real number and the other real number) and the other real number
(=> (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 778-789	If the previous month of a kind of month in year a year is another kind of month another year and the year is an instance of the year an integer and equal a kind of month and the month January, then equal another kind of month and December and the other year is an instance of the year (the integer and 1)
(=> (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 18111-18136	If the relative angle between an object and another object is a real number and one end of the object is a third object and one end of the object is a fourth object and equal the third object and the fourth object and the length of the object is the real number1 an unit of measure(s) and the length of the other object is the real number2 the unit of measure(s) and the distance between the third object and a fifth object is the real number3 the unit of measure(s) and one end of the other object is the fifth object and one end of the other object is a sixth object and equal the fifth object and the sixth object and the third object doesn't meet the fifth object, then equal the real number and the arccosine of ((the real number3 and the real number3 and the real number1 and the real number1) and the real number2 and the real number2) and 2.0 and the real number1 and the real number2
(=> (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 18678-18694	If a time duration amount as resource for the Process a process and the time duration is an instance of constant quantity and an object is a resource for the process and the measure of the object is a real number an unit of measure(s) holds during the beginning of the time of existence of the process and the measure of the object is another real number the unit of measure(s) holds during the end of the time of existence of the process, then equal the time duration and (the real number and the other real number) the unit of measure(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 18734-18760	If a function quantity amount as resource for the Process a process and the function quantity is an instance of function quantity and an object is a resource for the process and equal the function quantity and the per of a real number an unit of measure(s) and another real number another unit of measure(s) and duration of the time of existence of the process is a third real number the other unit of measure(s) and the measure of the object is a fourth real number the unit of measure(s) holds during the beginning of the time of existence of the process and the measure of the object is a time duration the unit of measure(s) holds during the end of the time of existence of the process, then equal the time duration and (the fourth real number and the third real number and the real number and the other real number) the unit of measure(s)

statement

(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32.0) 1.8) FahrenheitDegree))	Merge.kif 7062-7064	equal a real number celsius degree(s) and (the real number and 32.0) and 1.8 fahrenheit degree(s)
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree))	Merge.kif 7058-7060	equal a real number celsius degree(s) and (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 1000-1013	equal the reaching military age annually male of a geopolitical area and a year and the number of instances in the class described by a symbolic string
(forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1)))	Merge.kif 4789-4790	For all an integer equal (the integer+2) and (the integer and 1)

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

KB Term:			Term intersection

English Word: