inList - Sigma Knowledge base Browser

appearance as argument number 1

(documentation inList ChineseLanguage "这是类似 List 的 element 和 instance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如： (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的")	chinese_format.kif 1973-1975
(documentation inList EnglishLanguage "The analog of element and instance for Lists. (inList ?OBJ ?LIST) means that ?OBJ is in the List ?LIST. For example, (inList Tuesday (ListFn Monday Tuesday Wednesday)) would be true.")	Merge.kif 3110-3112
(documentation inList JapaneseLanguage "Lists の element と instance のアナログ。 (inList ?OBJ ?LIST)とは、?OBJ が List ?LIST 内であることを意味する。例： (inList Tuesday (ListFn Monday Tuesday Wednesday)) は正しい。")	japanese_format.kif 605-607
(domain inList 1 Entity)	Merge.kif 3107-3107	The number 1 argument of in list is an instance of entity
(domain inList 2 List)	Merge.kif 3108-3108	The number 2 argument of in list is an instance of list
(instance inList BinaryPredicate)	Merge.kif 3105-3105	in list is an instance of binary predicate
(instance inList PartialValuedRelation)	Merge.kif 3106-3106	in list is an instance of partial valued relation

appearance as argument number 2

(format ChineseLanguage inList "%1 %n 是 %2 的 member")	chinese_format.kif 131-131
(format EnglishLanguage inList "%1 is %n a member of %2")	english_format.kif 132-132
(format FrenchLanguage inList "%1 est %n un membre de %2")	french_format.kif 87-87
(format ItalianLanguage inList "%1 è %n un è membro di %2")	relations-it.txt 147-147
(format JapaneseLanguage inList "%1 は %2 の member では %n")	japanese_format.kif 1914-1914
(format PortugueseLanguage inList "%1 e' %n um membro de %2")	portuguese_format.kif 39-39
(format cz inList "%1 %p{je} %n{nen�} a member of %2")	relations-cz.txt 103-103
(format de inList "%1 ist ein Mitglied von %2")	relations-de.txt 157-157
(format hi inList "%1 %2 kaa sadasya %n hai")	relations-hindi.txt 186-186
(format ro inList "%1 %n{nu} este un member%t{element} al lui %2")	relations-ro.kif 106-106
(format sv inList "%1 är %n{inte} en medlem i %2")	relations-sv.txt 86-86
(format tg inList "%1 %n ay ang kasapi ng %2")	relations-tg.txt 298-298
(subrelation albumTrack inList)	Music.kif 332-332	album track is a subrelation of in list
(termFormat ChineseLanguage inList "在列表中")	domainEnglishFormat.kif 30227-30227	album track is a subrelation of in list
(termFormat ChineseLanguage inList "在列表内")	chinese_format.kif 132-132	album track is a subrelation of in list
(termFormat ChineseTraditionalLanguage inList "在列表中")	domainEnglishFormat.kif 30226-30226	album track is a subrelation of in list
(termFormat EnglishLanguage inList "in list")	domainEnglishFormat.kif 30225-30225	album track is a subrelation of in list
(termFormat de inList "inListe")	terms-de.txt 47-47	album track is a subrelation of in list
(termFormat tg inList "sa mula")	relations-tg.txt 299-299	album track is a subrelation of in list

antecedent

(=> (and (equal ?A (AverageFn ?L)) (inList ?N ?L)) (instance ?N Number))	Merge.kif 3287-3291	If a real number is equal to the average of the numbers in a list and an entity is a member of the list, then the entity is an instance of number
(=> (and (equal ?SPEEDLIST (Mean3SecondWindSpeedListFn ?PLACE ?TIME)) (inList ?SPEED ?SPEEDLIST)) (exists (?TIMELIST ?INT) (and (equal ?TIMELIST (TimeIntervalListFn ?TIME (MeasureFn 3 SecondDuration))) (inList ?INT ?TIMELIST) (equal ?SPEED (Mean3SecondWindSpeedFn ?PLACE ?INT)))))	Weather.kif 1988-2000	If a list is equal to Mean3SecondWindSpeedListFn ending at a time interval in region a geographic area and a function quantity is a member of the list, then there exist the time intervalLIST and another time interval such that the time intervalLIST is equal to ConsecutiveTimeIntervalList for at the time interval at 3 second duration(s) is contained in TimeIntervalListFn and the other time interval is a member of the time intervalLIST and the function quantity is equal to Mean3SecondWindSpeedFn for the other time interval in region the geographic area
(=> (and (equal ?SPEEDLIST (Mean3SecondWindSpeedListFn ?PLACE ?TIME)) (inList ?SPEED ?SPEEDLIST)) (instance ?SPEED FunctionQuantity))	Weather.kif 1981-1986	If a list is equal to Mean3SecondWindSpeedListFn ending at a time interval in region a geographic area and an entity is a member of the list, then the entity is an instance of function quantity
(=> (and (exhaustiveAttribute ?CLASS @ROW) (inList ?ATTR (ListFn @ROW))) (instance ?ATTR ?CLASS))	Merge.kif 503-507	If @ROW are all the attributes of another kind of attribute and an entity is a member of (@ROW), then the entity is an instance of another kind of attribute
(=> (and (exhaustiveAttribute ?CLASS @ROW) (inList ?ATTR (ListFn @ROW))) (instance ?ATTR Attribute))	Merge.kif 497-501	If @ROW are all the attributes of another kind of attribute and an entity is a member of (@ROW), then the entity is an instance of attribute
(=> (and (inList ?E ?L) (equal ?L (AmountsFn ?S ?CO ?U))) (instance ?E RationalNumber))	Merge.kif 7583-7588	If an entity is a member of a list and the list is equal to Amounts fn a kind of substance, a corpuscular object and an unit of mass, then the entity is an instance of rational number
(=> (and (inList ?INT ?LIST) (equal ?LIST (TimeIntervalListFn ?TIME ?DUR))) (duration ?INT ?DUR))	Weather.kif 1958-1963	If a time interval is a member of a consecutive time interval list and the consecutive time interval list is equal to ConsecutiveTimeIntervalList for at another time interval at a time duration is contained in TimeIntervalListFn, then duration of the time interval is the time duration
(=> (and (inList ?INT ?LIST) (equal ?LIST (TimeIntervalListFn ?TIME ?DUR))) (equal (BeginFn ?TIME) (BeginFn (FirstFn ?LIST))))	Weather.kif 1949-1956	If an entity is a member of a consecutive time interval list and the consecutive time interval list is equal to ConsecutiveTimeIntervalList for at a time interval at a time duration is contained in TimeIntervalListFn, then the beginning of the time interval is equal to the beginning of the first of the consecutive time interval list
(=> (and (inList ?ITEM ?RESULTS) (instance ?RESULTS SRPResults)) (exists (?SRP) (and (instance ?SRP SearchResultsPage) (component ?RESULTS ?SRP))))	UXExperimentalTerms.kif 2491-2498	If an entity is a member of a list and the list is an instance of search results, then there exists a corpuscular object such that the corpuscular object is an instance of search results page and the list is a component of the corpuscular object
(=> (and (inList ?ITEM ?RESULTS) (instance ?RESULTS SRPResults)) (or (instance ?ITEM WebListing) (instance ?ITEM WebPage)))	UXExperimentalTerms.kif 2483-2489	If an entity is a member of a list and the list is an instance of search results, then the entity is an instance of web listing or the entity is an instance of web page
(=> (and (instance ?LIST ConsecutiveTimeIntervalList) (inList ?TIME ?LIST)) (instance ?Time TimeInterval))	Weather.kif 1912-1916	If a list is an instance of consecutive time interval list and an entity is a member of the list, then another entity is an instance of time interval
(=> (and (instance ?LIST MeasuringList) (inList ?M ?LIST)) (instance ?M Measuring))	Weather.kif 1699-1703	If a list is an instance of measuring list and an entity is a member of the list, then the entity is an instance of measuring
(=> (and (instance ?LIST MeasuringResultList) (inList ?R ?LIST)) (instance ?R PhysicalQuantity))	Weather.kif 1767-1771	If a list is an instance of measuring result list and an entity is a member of the list, then the entity is an instance of physical quantity
(=> (and (instance ?LIST MeasuringSurfaceWindSpeedList) (inList ?M ?LIST)) (instance ?M SurfaceWindSpeedMeasuring))	Weather.kif 1733-1737	If a list is an instance of measuring surface wind speed list and an entity is a member of the list, then the entity is an instance of surface wind speed measuring
(=> (and (instance ?LIST NumberList) (inList ?NUM ?LIST)) (instance ?NUM Number))	Weather.kif 1802-1806	If a list is an instance of number list and an entity is a member of the list, then the entity is an instance of number
(=> (and (instance ?REL IntentionalRelation) (?REL ?AGENT @ROW) (inList ?OBJ (ListFn @ROW))) (inScopeOfInterest ?AGENT ?OBJ))	Merge.kif 2677-2682	If an entity is an instance of intentional relation and the entity a cognitive agent and @ROW and a third entity is a member of (@ROW), then the cognitive agent is interested in the third entity
(=> (and (locationMeasuringList ?LIST ?PLACE) (inList ?M ?LIST)) (and (instance ?M Measuring) (eventLocated ?M ?PLACE)))	Weather.kif 1752-1758	If The eventLocated for a measuring list is a geographic area and a process is a member of the measuring list, then the process is an instance of measuring and the process is located at the geographic area
(=> (and (measuringListInterval ?LIST ?DUR) (inList ?M ?LIST)) (duration (WhenFn ?M) ?DUR))	Weather.kif 1843-1847	If The Measuring for list a measuring list occurs at a time duration interval. and a physical is a member of the measuring list, then duration of the time of existence of the physical is the time duration
(=> (and (orientation ?OBJ1 ?OBJ2 ?ATTR1) (contraryAttribute @ROW) (inList ?ATTR1 (ListFn @ROW)) (inList ?ATTR2 (ListFn @ROW)) (not (equal ?ATTR1 ?ATTR2))) (not (orientation ?OBJ1 ?OBJ2 ?ATTR2)))	Merge.kif 16992-17000	If an object is a positional attribute to another object and @ROW is the opposite of and the positional attribute is a member of (@ROW) and another positional attribute is a member of (@ROW) and the positional attribute is not equal to the other positional attribute, then the object is not the other positional attribute to the other object
(=> (and (processList @ROW) (inList ?Process1 (ListFn @ROW)) (inList ?Process2 (ListFn @ROW)) (equal (ListOrderFn (ListFn @ROW) ?Number1) ?Process1) (equal (ListOrderFn (ListFn @ROW) ?Number2) ?Process2) (lessThan ?Number1 ?Number2)) (earlier (WhenFn ?Process1) (WhenFn ?Process2)))	QoSontology.kif 694-710	If the list of processes @ROW and a physical is a member of (@ROW) and another physical is a member of (@ROW) and another entity element of (@ROW) is equal to the physical and a third entity element of (@ROW) is equal to the other physical and a positive integer is less than another positive integer, then the time of existence of the physical happens earlier than the time of existence of the other physical
(=> (and (viewedItemList ?USER ?LIST) (inList ?ACCESSING ?LIST)) (and (instance ?ACCESSING AccessingWebPage) (agent ?ACCESSING ?USER) (exists (?DEST) (and (instance ?DEST WebPage) (destination ?ACCESSING WebPage)))))	UXExperimentalTerms.kif 771-781	If a list is the list of items viewed by an agent and a process is a member of the list, then the process is an instance of accessing web page and the agent is an agent of the process and there exists an entity such that the entity is an instance of web page and the process ends up at web page
(=> (inList ?ITEM ?LIST) (exists (?NUMBER) (equal (ListOrderFn ?LIST ?NUMBER) ?ITEM)))	Merge.kif 3114-3117	If an entity is a member of a list, then there exists a positive integer such that the positive integerth element of the list is equal to the entity

consequent

(<=> (and (instance ?Y (YearFn ?YEAR)) (equal (MaleLifeExpectancyAtBirthFn ?AREA ?Y) ?REALNUMBER)) (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (attribute ?INDIVIDUAL Male) (during (WhenFn ?BIRTH) ?Y) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER))))	People.kif 357-390	A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
(<=> (and (instance ?YEAR (YearFn ?Y)) (equal (FemaleLifeExpectancyAtBirthFn ?AREA ?YEAR) ?REALNUMBER)) (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (attribute ?INDIVIDUAL Female) (during (WhenFn ?BIRTH) ?YEAR) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER))))	People.kif 403-436	A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
(<=> (and (instance ?YEAR (YearFn ?Y)) (equal (LifeExpectancyAtBirthFn ?AREA ?YEAR) ?REALNUMBER)) (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH) (and (instance ?LIST List) (instance (ListLengthFn ?LIST) ?COUNT) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (and (instance ?LISTITEM ?LIFEEXPECTANCYAGE) (not (exists (?NUMBER) (and (instance ?NUMBER ?LIFEEXPECTANCYAGE) (not (inList ?NUMBER ?LIST))))) (equal ?COUNT (CardinalityFn (KappaFn ?LIFEEXPECTANCYAGE (and (instance ?BIRTH Birth) (experiencer ?BIRTH ?INDIVIDUAL) (instance ?INDIVIDUAL Human) (during (WhenFn ?BIRTH) ?YEAR) (equal (WhereFn ?BIRTH (WhenFn ?BIRTH)) ?AREA) (instance ?DEATH Death) (experiencer ?DEATH ?INDIVIDUAL) (holdsDuring (WhenFn ?DEATH) (age ?INDIVIDUAL (MeasureFn ?LIFEEXPECTANCYAGE YearDuration)))))))))) (average ?LIST ?REALNUMBER))))	People.kif 310-342	A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
(<=> (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 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 another positive integer if the other positive integer is a member of the other list, then there exist another real number, the other real numberMINUSONE,, , a third positive integer and a fourth positive integer such that the other real number is greater than 1 and the other real number is less than or equal to length of the other list and the other positive integerth element of the other list is equal to the other real number and the third positive integer is a member of the list and the other real number is equal to the third positive integerth element of the list and the fourth positive integer is a member of the other list and the other real numberMINUSONE is equal to (the other real number and 1) and the other real numberMINUSONE is equal to the fourth positive integerth element of the other list and the other positive integer is equal to (the third positive integer and the fourth positive integer) and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer
(=> (albumArtist ?A ?P) (exists (?R ?M) (and (instance ?R Recording) (inList ?R ?A) (record ?R ?M) (agent ?M ?P))))	Music.kif 280-287	If a cognitive agent is a performer on an album, then there exist a content bearing object and a process such that the content bearing object is an instance of recording and the content bearing object is a member of the album and the content bearing object is a record of the process and the cognitive agent is an agent of the process
(=> (and (amount ?S ?CO (MeasureFn ?N ?U)) (instance ?SI ?S) (measure ?SI (MeasureFn ?N2 ?U)) (part ?SI ?CO)) (exists (?L) (and (inList (MeasureFn ?N2 ?U) ?L) (equal ?L (AmountsFn ?S ?CO ?U)) (equal ?N (ListSumFn ?L)))))	Merge.kif 7597-7612	If amount a kind of substance, a corpuscular object and a real number an unit of mass(s) and a kind of substanceI is an instance of the kind of substance and the measure of the kind of substanceI is the real number2 the unit of mass(s) and the kind of substanceI is a part of the corpuscular object, then there exists a list such that the real number2 the unit of mass(s) is a member of the list and the list is equal to Amounts fn the kind of substance, the corpuscular object and the unit of mass and the real number is equal to the sum of the list
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0))))	Merge.kif 4862-4873	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the other integer mod the integer is equal to 0
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0)))))))	Merge.kif 4875-4889	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer if the third integer is a member of (@ROW), then the third integer mod the other integer is equal to 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0))))	Merge.kif 4947-4957	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the integer mod the other integer is equal to 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0)))))))	Merge.kif 4959-4973	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is less than the integer and for all a third integer if the third integer is a member of (@ROW), then the other integer mod the third integer is equal to 0
(=> (and (equal ?D (AlbumCopiesFn ?A ?DS)) (instance ?X ?D)) (forall (?S) (=> (inList ?S ?A) (exists (?C) (and (copy ?C ?S) (stored ?C ?X))))))	Music.kif 936-946	If a kind of data storage device is equal to the set of copies on a kind of data storage deviceS of an album and a third data storage device is an instance of the kind of data storage device, then for all an object if the object is a member of the album, then there exists a content bearing object such that the content bearing object is a copy of the object and the content bearing object is stored on the third data storage device
(=> (and (equal ?SPEEDLIST (Mean3SecondWindSpeedListFn ?PLACE ?TIME)) (inList ?SPEED ?SPEEDLIST)) (exists (?TIMELIST ?INT) (and (equal ?TIMELIST (TimeIntervalListFn ?TIME (MeasureFn 3 SecondDuration))) (inList ?INT ?TIMELIST) (equal ?SPEED (Mean3SecondWindSpeedFn ?PLACE ?INT)))))	Weather.kif 1988-2000	If a list is equal to Mean3SecondWindSpeedListFn ending at a time interval in region a geographic area and a function quantity is a member of the list, then there exist the time intervalLIST and another time interval such that the time intervalLIST is equal to ConsecutiveTimeIntervalList for at the time interval at 3 second duration(s) is contained in TimeIntervalListFn and the other time interval is a member of the time intervalLIST and the function quantity is equal to Mean3SecondWindSpeedFn for the other time interval in region the geographic area
(=> (and (fleetDeadWeightTonnage ?FLEET (MeasureFn ?T LongTon)) (vesselDeadWeightTonnage ?VESSEL (MeasureFn ?X LongTon)) (member ?VESSEL ?FLEET)) (exists (?L) (and (instance ?L List) (inList ?X ?L) (equal ?T (ListSumFn ?L)))))	Transportation.kif 2729-2739	If a real number long ton(s) is a fleet dead weight tonnage of a collection and another real number long ton(s) is a vessel dead weight tonnage of a water vehicle and the water vehicle is a member of the collection, then there exists a list such that the list is an instance of list and the other real number is a member of the list and the real number is equal to the sum of the list
(=> (and (instance ?OBJ DigitalDataStorageDevice) (part ?PART ?OBJ) (instance ?PART DigitalData)) (exists (?SCHEME ?LIST ?NUM) (and (codeMapping ?SCHEME ?PART ?NUM) (represents ?LIST ?SCHEME) (=> (inList ?NUM ?LIST) (instance ?NUM BinaryNumber)))))	Media.kif 801-812	If an object is an instance of digital data storage device and a symbolic string is a part of the object and the symbolic string is an instance of digital data, then there exist a code map, a list and an entity such that the symbolic string in the code map denotes the entity and the list expresses the code map and if the entity is a member of the list, then the entity is an instance of binary number
(=> (and (instance ?WW WaterWave) (waveHeight ?WW ?WH)) (exists (?LIST ?WA ?U ?SWH) (and (inList ?WH ?LIST) (instance ?WA WaterArea) (eventLocated ?WW ?WA) (instance ?U UnitOfLength) (significantWaveHeight ?WA (WhenFn ?WW) (MeasureFn ?SWH ?U)) (equal ?SWH (MultiplicationFn 4.0 (StandardDeviationFn ?LIST))))))	Weather.kif 1515-1530	If a water wave is an instance of water wave and The waveHeight of the water wave a length measure., then there exist a list, a water area,, , an unit of measure and a real number such that the length measure is a member of the list and the water area is an instance of water area and the water wave is located at the water area and the unit of measure is an instance of unit of length and significantWaveHeight in the water area during the time of existence of the water wave is the real number the unit of measure(s). and the real number is equal to 4.0 and The StandardDeviationFn of the list
(=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber))))	Merge.kif 5370-5375	If a real number is an average of a list, then for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of real number
(=> (contraryAttribute @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Attribute)))	Merge.kif 464-468	If @ROW is the opposite of , then if another entity is a member of (@ROW), then the other entity is an instance of attribute
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS))))	Merge.kif 2951-2956	If a class is disjointly decomposed into @ROW, then for all a third class if the third class is a member of (@ROW), then the third class is a subclass of the class
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM1 ?ITEM2) (=> (and (inList ?ITEM1 (ListFn @ROW)) (inList ?ITEM2 (ListFn @ROW)) (not (equal ?ITEM1 ?ITEM2))) (disjoint ?ITEM1 ?ITEM2))))	Merge.kif 2958-2967	If a class is disjointly decomposed into @ROW, then for all a third class and a fourth class if the third class is a member of (@ROW) and the fourth class is a member of (@ROW) and the third class is not equal to the fourth class, then the third class is disjoint from the fourth class
(=> (disjointDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class)))	Merge.kif 574-578	If @ROW is disjointly decomposed into @ROW, then if another entity is a member of (@ROW), then the other entity is an instance of class
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number)))	Merge.kif 4855-4860	If the greatest common divisor of @ROW is equal to an integer, then if another entity is a member of (@ROW), then the other entity is an instance of number
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number)))	Merge.kif 4940-4945	If the least common multiple of @ROW is equal to an integer, then if another entity is a member of (@ROW), then the other entity is an instance of number
(=> (equal ?X (MaxValueFn ?LIST)) (not (exists (?Y) (and (inList ?Y ?LIST) (greaterThan ?Y ?X)))))	Weather.kif 1668-1675	If a real number is equal to The maximum value of the a list, then there doesn't exist another real number such that the other real number is a member of the list and the other real number is greater than the real number
(=> (exhaustiveAttribute ?CLASS @ROW) (forall (?ATTR1) (=> (instance ?ATTR1 ?CLASS) (exists (?ATTR2) (and (inList ?ATTR2 (ListFn @ROW)) (equal ?ATTR1 ?ATTR2))))))	Merge.kif 509-517	If @ROW are all the attributes of another kind of attribute, then for all an entity if the entity is an instance of another kind of attribute, then there exists another entity such that the other entity is a member of (@ROW) and the entity is equal to the other entity
(=> (exhaustiveDecomposition ?CLASS @ROW) (forall (?OBJ) (=> (instance ?OBJ ?CLASS) (exists (?ITEM) (and (inList ?ITEM (ListFn @ROW)) (instance ?OBJ ?ITEM))))))	Merge.kif 2941-2949	If a class is covered by @ROW, then for all an entity if the entity is an instance of the class, then there exists a third class such that the third class is a member of (@ROW) and the entity is an instance of the third class

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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

KB Term:			Term intersection

English Word: