Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
HerbaceousPlant
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
WoodyPlant
cb
cz
de
hi
ro
sv
tg
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
inList
Sigma KEE - inList
inList
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
List
s. (
inList
?OBJ ?LIST) means that ?OBJ is in the
List
?LIST. For example, (
inList
Tuesday
(
ListFn
Monday
Tuesday
Wednesday
)) would be true.")
Merge.kif 3109-3111
(
documentation
inList
JapaneseLanguage
"
List
s の
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 3106-3106
Le nombre 1 argument de
inList
est une
instance
de
entit�
(
domain
inList
2
List
)
Merge.kif 3107-3107
Le nombre 2 argument de
inList
est une
instance
de
liste
(
instance
inList
BinaryPredicate
)
Merge.kif 3104-3104
inList
est une
instance
de
pr�dicat binaire
(
instance
inList
PartialValuedRelation
)
Merge.kif 3105-3105
inList
est une
instance
de
relation partielle
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
albumTrack
est une
sous
-relation de
inList
(
termFormat
ChineseLanguage
inList
"在列表中")
domainEnglishFormat.kif 30193-30193
(
termFormat
ChineseLanguage
inList
"在列表内")
chinese_format.kif 132-132
(
termFormat
ChineseTraditionalLanguage
inList
"在列表中")
domainEnglishFormat.kif 30192-30192
(
termFormat
EnglishLanguage
inList
"in list")
domainEnglishFormat.kif 30191-30191
(
termFormat
de
inList
"inListe")
terms-de.txt 47-47
(
termFormat
tg
inList
"sa mula")
relations-tg.txt 299-299
antecedent
(=>
(
and
(
equal
?A
(
AverageFn
?L))
(
inList
?N ?L))
(
instance
?N
Number
))
Merge.kif 3286-3290
Nombre r�el
est
AverageFn
liste
entit�
est un
membre
de
liste
entit�
est une
instance
de
nombre
(=>
(
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 2005-2017
Liste
est
Mean3SecondWindSpeedListFn
secteur g�ographique
and
interval temporel
function de quantit�
est un
membre
de
liste
interval temporel
LIST
interval temporel
interval temporel
LIST est
TimeIntervalListFn
interval temporel
and 3
SecondDuration
(s)
interval temporel
est un
membre
de
interval temporel
LIST
function de quantit�
est
Mean3SecondWindSpeedFn
secteur g�ographique
and
interval temporel
(=>
(
and
(
equal
?SPEEDLIST
(
Mean3SecondWindSpeedListFn
?PLACE ?TIME))
(
inList
?SPEED ?SPEEDLIST))
(
instance
?SPEED
FunctionQuantity
))
Weather.kif 1998-2003
Liste
est
Mean3SecondWindSpeedListFn
secteur g�ographique
and
interval temporel
entit�
est un
membre
de
liste
entit�
est une
instance
de
function de quantit�
(=>
(
and
(
exhaustiveAttribute
?CLASS @ROW)
(
inList
?ATTR
(
ListFn
@ROW)))
(
instance
?ATTR ?CLASS))
Merge.kif 503-507
exhaustiveAttribute
attribut
and @ROW
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
attribut
(=>
(
and
(
exhaustiveAttribute
?CLASS @ROW)
(
inList
?ATTR
(
ListFn
@ROW)))
(
instance
?ATTR
Attribute
))
Merge.kif 497-501
exhaustiveAttribute
attribut
and @ROW
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
attribut
(=>
(
and
(
inList
?E ?L)
(
equal
?L
(
AmountsFn
?S ?CO ?U)))
(
instance
?E
RationalNumber
))
Merge.kif 7582-7587
Entit�
est un
membre
de
liste
liste
est
AmountsFn
substance
,
objet corpusculaire
and
UnitOfMass
entit�
est une
instance
de
nombre rationnel
(=>
(
and
(
inList
?INT ?LIST)
(
equal
?LIST
(
TimeIntervalListFn
?TIME ?DUR)))
(
duration
?INT ?DUR))
Weather.kif 1975-1980
Interval temporel
est un
membre
de
ConsecutiveTimeIntervalList
ConsecutiveTimeIntervalList
est
TimeIntervalListFn
interval temporel
and
dur�e temporel
la
dur
�� de
interval temporel
est
dur�e temporel
(=>
(
and
(
inList
?INT ?LIST)
(
equal
?LIST
(
TimeIntervalListFn
?TIME ?DUR)))
(
equal
(
BeginFn
?TIME)
(
BeginFn
(
FirstFn
?LIST))))
Weather.kif 1966-1973
Entit�
est un
membre
de
ConsecutiveTimeIntervalList
ConsecutiveTimeIntervalList
est
TimeIntervalListFn
interval temporel
and
dur�e temporel
le
d
�but de
interval temporel
est
d
�but de
FirstFn
ConsecutiveTimeIntervalList
(=>
(
and
(
inList
?ITEM ?RESULTS)
(
instance
?RESULTS
SRPResults
))
(
exists
(?SRP)
(
and
(
instance
?SRP
SearchResultsPage
)
(
component
?RESULTS ?SRP))))
UXExperimentalTerms.kif 2491-2498
Entit�
est un
membre
de
liste
liste
est une
instance
de
SRPResults
objet corpusculaire
objet corpusculaire
est une
instance
de
SearchResultsPage
liste
est un
composant
de
objet corpusculaire
(=>
(
and
(
inList
?ITEM ?RESULTS)
(
instance
?RESULTS
SRPResults
))
(
or
(
instance
?ITEM
WebListing
)
(
instance
?ITEM
WebPage
)))
UXExperimentalTerms.kif 2483-2489
Entit�
est un
membre
de
liste
liste
est une
instance
de
SRPResults
entit�
est une
instance
de
WebListing
entit�
est une
instance
de
WebPage
(=>
(
and
(
instance
?LIST
ConsecutiveTimeIntervalList
)
(
inList
?TIME ?LIST))
(
instance
?Time
TimeInterval
))
Weather.kif 1929-1933
Liste
est une
instance
de
ConsecutiveTimeIntervalList
entit�
est un
membre
de
liste
entit�
est une
instance
de
interval temporel
(=>
(
and
(
instance
?LIST
MeasuringList
)
(
inList
?M ?LIST))
(
instance
?M
Measuring
))
Weather.kif 1716-1720
Liste
est une
instance
de
MeasuringList
entit�
est un
membre
de
liste
entit�
est une
instance
de
mesurer
(=>
(
and
(
instance
?LIST
MeasuringResultList
)
(
inList
?R ?LIST))
(
instance
?R
PhysicalQuantity
))
Weather.kif 1784-1788
Liste
est une
instance
de
MeasuringResultList
entit�
est un
membre
de
liste
entit�
est une
instance
de
quantit� physique
(=>
(
and
(
instance
?LIST
MeasuringSurfaceWindSpeedList
)
(
inList
?M ?LIST))
(
instance
?M
SurfaceWindSpeedMeasuring
))
Weather.kif 1750-1754
Liste
est une
instance
de
MeasuringSurfaceWindSpeedList
entit�
est un
membre
de
liste
entit�
est une
instance
de
SurfaceWindSpeedMeasuring
(=>
(
and
(
instance
?LIST
NumberList
)
(
inList
?NUM ?LIST))
(
instance
?NUM
Number
))
Weather.kif 1819-1823
Liste
est une
instance
de
NumberList
entit�
est un
membre
de
liste
entit�
est une
instance
de
nombre
(=>
(
and
(
instance
?REL
IntentionalRelation
)
(?REL ?AGENT @ROW)
(
inList
?OBJ
(
ListFn
@ROW)))
(
inScopeOfInterest
?AGENT ?OBJ))
Merge.kif 2677-2682
Entit�
est une
instance
de
IntentionalRelation
entit�
agent cognitif
and @ROW
entit�
est un
membre
de (@ROW)
agent cognitif
est
interess
� par
entit�
(=>
(
and
(
locationMeasuringList
?LIST ?PLACE)
(
inList
?M ?LIST))
(
and
(
instance
?M
Measuring
)
(
eventLocated
?M ?PLACE)))
Weather.kif 1769-1775
locationMeasuringList
MeasuringList
and
secteur g�ographique
processus
est un
membre
de
MeasuringList
processus
est une
instance
de
mesurer
eventLocated
processus
and
secteur g�ographique
(=>
(
and
(
measuringListInterval
?LIST ?DUR)
(
inList
?M ?LIST))
(
duration
(
WhenFn
?M) ?DUR))
Weather.kif 1860-1864
measuringListInterval
MeasuringList
and
dur�e temporel
physique
est un
membre
de
MeasuringList
la
dur
�� de
temps
d'existence de
physique
est
dur�e temporel
(=>
(
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 16921-16929
Objet
est
attribut positionnel
�
objet
@ROW est
l
'oppos� de
attribut positionnel
est un
membre
de (@ROW)
attribut positionnel
est un
membre
de (@ROW)
attribut positionnel
est
attribut positionnel
objet
est
attribut positionnel
�
objet
(=>
(
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
processList
@ROW
physique
est un
membre
de (@ROW)
physique
est un
membre
de (@ROW)
entit�
physique
entit�
physique
nombre entier positif
est
moins
que
nombre entier positif
temps
d'existence de
physique
arrive
plus
t�t que
temps
d'existence de
physique
(=>
(
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
viewedItemList
AutonomousAgent
and
liste
processus
est un
membre
de
liste
processus
est une
instance
de
AccessingWebPage
processus
est un
agent
de
AutonomousAgent
entit�
entit�
est une
instance
de
WebPage
processus
aboutit
�
WebPage
(=>
(
inList
?ITEM ?LIST)
(
exists
(?NUMBER)
(
equal
(
ListOrderFn
?LIST ?NUMBER) ?ITEM)))
Merge.kif 3113-3116
Entit�
est un
membre
de
liste
nombre entier positif
nombre entier positif
th
liste
est
entit�
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
Ann�e
est une
instance
de l'
ann
�e
ann�e
EAR
MaleLifeExpectancyAtBirthFn
secteur g�opolitique
and
ann�e
est
nombre r�el
liste
nombre entier
,
cha�ne sympbolique
,
entit�
,
entit�
and
entit�
liste
est une
instance
de
liste
longueur
de
liste
est une
instance
de
nombre entier
liste
ITEM
liste
ITEM est un
membre
de
liste
liste
ITEM est une
instance
de
cha�ne sympbolique
entit�
entit�
est une
instance
de
cha�ne sympbolique
entit�
est un
membre
de
liste
nombre entier
est
instances
dans la
classe
d�crite par
cha�ne sympbolique
average
liste
and
nombre r�el
(<=>
(
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
Ann�e
est une
instance
de l'
ann
�e
nombre entier
FemaleLifeExpectancyAtBirthFn
secteur g�opolitique
and
ann�e
est
nombre r�el
liste
nombre entier
,
cha�ne sympbolique
,
entit�
,
entit�
and
entit�
liste
est une
instance
de
liste
longueur
de
liste
est une
instance
de
nombre entier
liste
ITEM
liste
ITEM est un
membre
de
liste
liste
ITEM est une
instance
de
cha�ne sympbolique
entit�
entit�
est une
instance
de
cha�ne sympbolique
entit�
est un
membre
de
liste
nombre entier
est
instances
dans la
classe
d�crite par
cha�ne sympbolique
average
liste
and
nombre r�el
(<=>
(
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
Ann�e
est une
instance
de l'
ann
�e
nombre entier
LifeExpectancyAtBirthFn
secteur g�opolitique
and
ann�e
est
nombre r�el
liste
nombre entier
,
cha�ne sympbolique
,
entit�
,
entit�
and
entit�
liste
est une
instance
de
liste
longueur
de
liste
est une
instance
de
nombre entier
liste
ITEM
liste
ITEM est un
membre
de
liste
liste
ITEM est une
instance
de
cha�ne sympbolique
entit�
entit�
est une
instance
de
cha�ne sympbolique
entit�
est un
membre
de
liste
nombre entier
est
instances
dans la
classe
d�crite par
cha�ne sympbolique
average
liste
and
nombre r�el
(<=>
(
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
average
liste
and
nombre r�el
liste
nombre entier positif
longueur
de
liste
est
longueur
de
liste
1th
liste
est
liste
nombre entier positif
nombre entier positif
est un
membre
de
liste
nombre r�el
nombre r�el
MINUSONE,
nombre entier positif
and
nombre entier positif
nombre r�el
est
plus
grand
que 1
nombre r�el
est plus
petit
ou �gal �
longueur
de
liste
nombre entier positif
th
liste
est
nombre r�el
nombre entier positif
est un
membre
de
liste
nombre r�el
est
nombre entier positif
th
liste
nombre entier positif
est un
membre
de
liste
nombre r�el
MINUSONE est
nombre r�el
+ 1)
nombre r�el
MINUSONE est
nombre entier positif
th
liste
nombre entier positif
est
nombre entier positif
+
nombre entier positif
)
nombre entier positif
est
longueur
de
liste
nombre r�el
est
nombre entier positif
th
liste
+
nombre entier positif
(=>
(
albumArtist
?A ?P)
(
exists
(?R ?M)
(
and
(
instance
?R
Recording
)
(
inList
?R ?A)
(
record
?R ?M)
(
agent
?M ?P))))
Music.kif 280-287
albumArtist
Album
and
agent cognitif
objet exprimant un sens
processus
objet exprimant un sens
est une
instance
de
Recording
objet exprimant un sens
est un
membre
de
Album
record
objet exprimant un sens
and
processus
processus
est un
agent
de
agent cognitif
(=>
(
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 7596-7611
amount
substance
,
objet corpusculaire
and
nombre r�el
UnitOfMass
(s)
substance
I est une
instance
de
substance
la
mesure
de
substance
I est
nombre r�el
2
UnitOfMass
(s)
substance
I est une
partie
de
objet corpusculaire
liste
nombre r�el
2
UnitOfMass
(s) est un
membre
de
liste
liste
est
AmountsFn
substance
,
objet corpusculaire
and
UnitOfMass
nombre r�el
est
ListSumFn
liste
(=>
(
and
(
equal
(
GreatestCommonDivisorFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?ELEMENT ?NUMBER) 0))))
Merge.kif 4861-4872
Le
plus
grand diviseur commun de @ROW est
nombre entier
nombre entier
est
nombre entier
nombre entier
est un
membre
de (@ROW)
nombre entier
reste
nombre entier
est &%�gal � 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 4874-4888
Le
plus
grand diviseur commun de @ROW est
nombre entier
nombre entier
est
nombre entier
nombre entier
est
plus
grand
que
nombre entier
nombre entier
nombre entier
est un
membre
de (@ROW)
nombre entier
reste
nombre entier
est &%�gal � 0
(=>
(
and
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?NUMBER ?ELEMENT) 0))))
Merge.kif 4946-4956
La racine carr�e de
nombre
entier
de @ROW est
nombre entier
nombre entier
est
nombre entier
nombre entier
est un
membre
de (@ROW)
nombre entier
reste
nombre entier
est &%�gal � 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 4958-4972
La racine carr�e de
nombre
entier
de @ROW est
nombre entier
nombre entier
est
nombre entier
nombre entier
est
moins
que
nombre entier
nombre entier
nombre entier
est un
membre
de (@ROW)
nombre entier
reste
nombre entier
est &%�gal � 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
DataStorageDevice
est
AlbumCopiesFn
Album
and
DataStorageDevice
S
DataStorageDevice
est une
instance
de
DataStorageDevice
objet
objet
est un
membre
de
Album
objet exprimant un sens
objet exprimant un sens
est une
copie
exact de
objet
stored
objet exprimant un sens
and
DataStorageDevice
(=>
(
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 2005-2017
Liste
est
Mean3SecondWindSpeedListFn
secteur g�ographique
and
interval temporel
function de quantit�
est un
membre
de
liste
interval temporel
LIST
interval temporel
interval temporel
LIST est
TimeIntervalListFn
interval temporel
and 3
SecondDuration
(s)
interval temporel
est un
membre
de
interval temporel
LIST
function de quantit�
est
Mean3SecondWindSpeedFn
secteur g�ographique
and
interval temporel
(=>
(
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
Objet
est une
instance
de
DigitalDataStorageDevice
cha�ne sympbolique
est une
partie
de
objet
cha�ne sympbolique
est une
instance
de
DigitalData
CodeMap
liste
and
entit�
codeMapping
CodeMap
,
cha�ne sympbolique
and
entit�
liste
d
�finie
CodeMap
entit�
est un
membre
de
liste
entit�
est une
instance
de
nombre binaire
(=>
(
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 1532-1547
WaterWave
est une
instance
de
WaterWave
waveHeight
WaterWave
and
mesure de longueur
liste
plan d'eau
,
unit� de mesure
and
nombre r�el
mesure de longueur
est un
membre
de
liste
plan d'eau
est une
instance
de
plan d'eau
eventLocated
WaterWave
and
plan d'eau
unit� de mesure
est une
instance
de
UnitOfLength
significantWaveHeight
plan d'eau
,
temps
d'existence de
WaterWave
and
nombre r�el
unit� de mesure
(s)
nombre r�el
est
StandardDeviationFn
liste
(=>
(
average
?LIST ?AVERAGE)
(
forall
(?LISTITEM)
(=>
(
inList
?LISTITEM ?LIST)
(
instance
?LISTITEM
RealNumber
))))
Merge.kif 5369-5374
average
liste
and
nombre r�el
liste
ITEM
liste
ITEM est un
membre
de
liste
liste
ITEM est une
instance
de
nombre r�el
(=>
(
contraryAttribute
@ROW)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Attribute
)))
Merge.kif 464-468
@ROW est
l
'oppos� de
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
attribut
(=>
(
disjointDecomposition
?CLASS @ROW)
(
forall
(?ITEM)
(=>
(
inList
?ITEM
(
ListFn
@ROW))
(
subclass
?ITEM ?CLASS))))
Merge.kif 2950-2955
Classe
est
disjointement
decompos
� en @ROW
classe
classe
est un
membre
de (@ROW)
classe
est une
sous
-classe de
classe
(=>
(
disjointDecomposition
?CLASS @ROW)
(
forall
(?ITEM1 ?ITEM2)
(=>
(
and
(
inList
?ITEM1
(
ListFn
@ROW))
(
inList
?ITEM2
(
ListFn
@ROW))
(
not
(
equal
?ITEM1 ?ITEM2)))
(
disjoint
?ITEM1 ?ITEM2))))
Merge.kif 2957-2966
Classe
est
disjointement
decompos
� en @ROW
classe
classe
classe
est un
membre
de (@ROW)
classe
est un
membre
de (@ROW)
classe
est
classe
classe
est
disjoint
de
classe
(=>
(
disjointDecomposition
@ROW)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Class
)))
Merge.kif 574-578
@ROW est
disjointement
decompos
� en @ROW
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
classe
(=>
(
equal
(
GreatestCommonDivisorFn
@ROW) ?NUMBER)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Number
)))
Merge.kif 4854-4859
Le
plus
grand diviseur commun de @ROW est
nombre entier
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
nombre
(=>
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Number
)))
Merge.kif 4939-4944
La racine carr�e de
nombre
entier
de @ROW est
nombre entier
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
nombre
(=>
(
equal
?X
(
MaxValueFn
?LIST))
(
not
(
exists
(?Y)
(
and
(
inList
?Y ?LIST)
(
greaterThan
?Y ?X)))))
Weather.kif 1685-1692
Nombre r�el
est
MaxValueFn
liste
nombre r�el
nombre r�el
est un
membre
de
liste
nombre r�el
est
plus
grand
que
nombre r�el
(=>
(
exhaustiveAttribute
?CLASS @ROW)
(
forall
(?ATTR1)
(=>
(
instance
?ATTR1 ?CLASS)
(
exists
(?ATTR2)
(
and
(
inList
?ATTR2
(
ListFn
@ROW))
(
equal
?ATTR1 ?ATTR2))))))
Merge.kif 509-517
exhaustiveAttribute
attribut
and @ROW
entit�
entit�
est une
instance
de
attribut
entit�
entit�
est un
membre
de (@ROW)
entit�
est
entit�
(=>
(
exhaustiveDecomposition
?CLASS @ROW)
(
forall
(?OBJ)
(=>
(
instance
?OBJ ?CLASS)
(
exists
(?ITEM)
(
and
(
inList
?ITEM
(
ListFn
@ROW))
(
instance
?OBJ ?ITEM))))))
Merge.kif 2940-2948
Classe
est
couvert
par @ROW
entit�
entit�
est une
instance
de
classe
classe
classe
est un
membre
de (@ROW)
entit�
est une
instance
de
classe
(=>
(
exhaustiveDecomposition
@ROW)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Class
)))
Merge.kif 558-562
@ROW est
couvert
par @ROW
entit�
est un
membre
de (@ROW)
entit�
est une
instance
de
classe
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
Show simplified definition (without tree view)
Show simplified definition (with tree view)
Show without tree
Sigma web home
Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is
open source software
produced by
Articulate Software
and its partners