Browsing Interface
: Welcome guest :
log in
[
Home
| 
Graph
|  ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
Englishlanguage
FrenchLanguage
GermanLanguage
Hindi
ItalianLanguage
JapaneseLanguage
PortugueseLanguage
SpanishLanguage
SwedishLanguage
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
ListFn
Sigma KEE - ListFn
ListFn
appearance as argument number 1
(
documentation
ListFn
ChineseLanguage
"这是一个可以接受任何数量的参数,然后交出含有跟哪些参数完全 相同顺序的
Function
。")
chinese_format.kif 1962-1963
(
documentation
ListFn
EnglishLanguage
"A
Function
that takes any number of arguments and returns the
List
containing those arguments in exactly the same order.")
Merge.kif 2950-2951
(
documentation
ListFn
JapaneseLanguage
"任意の数の引数を受け取り、それらの引数を含む
List
を まったく同じ順序で返す
Function
。")
japanese_format.kif 594-595
(
domain
ListFn
1
Entity
)
Merge.kif 2946-2946
The number 1 argument of
list
is an
instance
of
entity
(
instance
ListFn
Function
)
Merge.kif 2944-2944
List
is an
instance
of
function
(
instance
ListFn
VariableArityRelation
)
Merge.kif 2945-2945
List
is an
instance
of
variable arity relation
(
range
ListFn
List
)
Merge.kif 2948-2948
The
range
of
list
is an instance of
list
appearance as argument number 2
(
format
ChineseLanguage
ListFn
"(%*[,])")
chinese_format.kif 261-261
(
format
EnglishLanguage
ListFn
"(%*[,])")
english_format.kif 266-266
(
format
FrenchLanguage
ListFn
"(%*[,])")
french_format.kif 149-149
(
format
ItalianLanguage
ListFn
"(%*[,]")
relations-it.txt 167-167
(
format
JapaneseLanguage
ListFn
"(%*[,])")
japanese_format.kif 1977-1977
(
format
PortugueseLanguage
ListFn
"(%*[,])")
portuguese_format.kif 101-101
(
format
cz
ListFn
"(%*[,])")
relations-cz.txt 158-158
(
format
de
ListFn
"(%*[,])")
relations-de.txt 336-336
(
format
hi
ListFn
"(%*[,]")
relations-hindi.txt 206-206
(
format
ro
ListFn
"(%*[,])")
relations-ro.kif 168-168
(
format
sv
ListFn
"(%*[,])")
relations-sv.txt 155-155
(
format
tg
ListFn
"(%*[,]")
relations-tg.txt 333-333
(
termFormat
ChineseLanguage
ListFn
"名单")
domainEnglishFormat.kif 34696-34696
(
termFormat
ChineseLanguage
ListFn
"表列函数")
chinese_format.kif 262-262
(
termFormat
ChineseTraditionalLanguage
ListFn
"名單")
domainEnglishFormat.kif 34695-34695
(
termFormat
EnglishLanguage
ListFn
"list")
domainEnglishFormat.kif 34694-34694
(
termFormat
de
ListFn
"ListeFn")
terms-de.txt 107-107
(
termFormat
tg
ListFn
"tungkulin ng talaan")
relations-tg.txt 334-334
antecedent
(=>
(
and
(
contraryAttribute
@ROW)
(
equal
?ATTR1
(
ListOrderFn
(
ListFn
@ROW) ?NUMBER1))
(
equal
?ATTR2
(
ListOrderFn
(
ListFn
@ROW) ?NUMBER2))
(
not
(
equal
?NUMBER1 ?NUMBER2))
(
property
?OBJ ?ATTR1))
(
not
(
property
?OBJ ?ATTR2)))
Merge.kif 469-477
If @ROW is the
opposite
of and
equal
an attribute
and
another entity
element
of (@ROW) and
equal
another attribute
and
a third entity
element
of (@ROW) and
equal
a positive integer
and
another positive integer
and
a fourth entity
the
attribute
the attribute
,
then
the fourth entity
does not have the
attribute
the other attribute
(=>
(
and
(
contraryAttribute
@ROW1)
(
identicalListItems
(
ListFn
@ROW1)
(
ListFn
@ROW2)))
(
contraryAttribute
@ROW2))
Merge.kif 463-467
If @ROW1 is the
opposite
of and (@ROW2) is an
identical
list items of (@ROW1),
then @ROW2 is the
opposite
of
(=>
(
and
(
defaultMaxValue
?REL ?ARG ?N)
(?REL @ARGS)
(
equal
?VAL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
modalAttribute
(
greaterThan
?N ?VAL)
Likely
))
Merge.kif 18633-18638
If The
defalutMaxValue
of
a predicate
with
a positive integer
arguments is
a quantity
. and
the predicate
@ARGS and
equal
another entity
and
the positive integer
th
element
of (@ARGS),
then the statement
the quantity
is
greater
than
the other entity
has the
modal
force
of
likely
(=>
(
and
(
defaultMinValue
?REL ?ARG ?N)
(?REL @ARGS)
(
equal
?VAL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
modalAttribute
(
greaterThan
?VAL ?N)
Likely
))
Merge.kif 18616-18621
If The
defaultMinValue
of
a predicate
with
a positive integer
arguments is
a quantity
. and
the predicate
@ARGS and
equal
another entity
and
the positive integer
th
element
of (@ARGS),
then the statement
the other entity
is
greater
than
the quantity
has the
modal
force
of
likely
(=>
(
and
(
defaultValue
?REL ?ARG ?N)
(?REL @ARGS)
(
equal
?VAL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
modalAttribute
(
equal
?N ?VAL)
Likely
))
Merge.kif 18650-18655
If The
defaultValue
of
a predicate
with
a positive integer
arguments is
a quantity
. and
the predicate
@ARGS and
equal
another entity
and
the positive integer
th
element
of (@ARGS),
then the statement
equal
the quantity
and
the other entity
has the
modal
force
of
likely
(=>
(
and
(
equal
?LIST1 ?LIST2)
(
equal
?LIST1
(
ListFn
@ROW1))
(
equal
?LIST2
(
ListFn
@ROW2)))
(
equal
(
ListOrderFn
(
ListFn
@ROW1) ?NUMBER)
(
ListOrderFn
(
ListFn
@ROW2) ?NUMBER)))
Merge.kif 289-296
If
equal
a list
and
another list
and
equal
the list
and (@ROW1) and
equal
the other list
and (@ROW2),
then
equal
a third entity
element
of (@ROW1) and
the third entity
element
of (@ROW2)
(=>
(
and
(
exactCardinality
?REL ?ARG 1)
(
instance
?REL
Predicate
)
(?REL @ARGS)
(
equal
?X
(
ListOrderFn
(
ListFn
@ARGS) ?ARG))
(
equal
?Y
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
equal
?X ?Y))
Media.kif 2108-2115
If there can be 1
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
and
the relation
@ARGS and
equal
another entity
and
the positive integer
th
element
of (@ARGS) and
equal
a fourth entity
and
the positive integer
th
element
of (@ARGS),
then
equal
the other entity
and
the fourth entity
(=>
(
and
(
exactCardinality
?REL ?ARG 1)
(
instance
?REL
Predicate
)
(?REL @ARGS)
(
equal
?X
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
not
(
exists
(?Y)
(
and
(
equal
?Y
(
ListOrderFn
(
ListFn
@ARGS) ?ARG))
(
not
(
equal
?X ?Y))))))
Media.kif 2095-2105
If there can be 1
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
and
the relation
@ARGS and
equal
another entity
and
the positive integer
th
element
of (@ARGS),
then there doesn't exist
a fourth entity
such that
equal
the fourth entity
and
the positive integer
th
element
of (@ARGS) and
equal
the other entity
and
the fourth entity
(=>
(
and
(
exhaustiveAttribute
?CLASS @ROW)
(
inList
?ATTR
(
ListFn
@ROW)))
(
instance
?ATTR ?CLASS))
Merge.kif 496-500
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 490-494
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
(
instance
(
LatitudeFn
?DIRECTION @ROW)
Region
)
(
equal
(
ListOrderFn
(
ListFn
@ROW) 1)
(
MeasureFn
?NUM
AngularDegree
)))
(
lessThanOrEqualTo
?NUM 90.0))
Geography.kif 597-601
If the
region
a directional attribute
of @ROW is an
instance
of
region
and
equal
1th
element
of (@ROW) and
a real number
angular degree
(s),
then
the real number
is
less
than or equal to 90.0
(=>
(
and
(
instance
(
LongitudeFn
?DIRECTION @ROW)
Region
)
(
equal
(
ListOrderFn
(
ListFn
@ROW) 1)
(
MeasureFn
?NUM
AngularDegree
)))
(
lessThanOrEqualTo
?NUM 180.0))
Geography.kif 637-644
If the
meridian
at @ROW
a directional attribute
is an
instance
of
region
and
equal
1th
element
of (@ROW) and
a real number
angular degree
(s),
then
the real number
is
less
than or equal to 180.0
(=>
(
and
(
instance
?REL
IntentionalRelation
)
(?REL ?AGENT @ROW)
(
inList
?OBJ
(
ListFn
@ROW)))
(
inScopeOfInterest
?AGENT ?OBJ))
Merge.kif 2688-2693
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
(
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 17096-17104
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
equal
the positional attribute
and
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 803-819
If the
list
of
processes
@ROW and
a physical
is a
member
of (@ROW) and
another physical
is a
member
of (@ROW) and
equal
another entity
element
of (@ROW) and
the physical
and
equal
a third entity
element
of (@ROW) and
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
consequent
(=>
(
and
(
domain
?REL ?NUMBER ?CLASS)
(
instance
?REL
Predicate
)
(?REL @ROW))
(
instance
(
ListOrderFn
(
ListFn
@ROW) ?NUMBER) ?CLASS))
Merge.kif 3011-3016
If the number
a positive integer
argument of
a relation
is an
instance
of
a class
and
the relation
is an
instance
of
predicate
and
the relation
@ROW,
then
the positive integer
th
element
of (@ROW) is an
instance
of
the class
(=>
(
and
(
domainSubclass
?REL ?NUMBER ?CLASS)
(
instance
?REL
Predicate
)
(?REL @ROW))
(
subclass
(
ListOrderFn
(
ListFn
@ROW) ?NUMBER) ?CLASS))
Merge.kif 3018-3023
If the number
a positive integer
argument of
a relation
is a
subclass
of
a class
and
the relation
is an
instance
of
predicate
and
the relation
@ROW,
then
the positive integer
th
element
of (@ROW) is a
subclass
of
the class
(=>
(
and
(
equal
(
GreatestCommonDivisorFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?ELEMENT ?NUMBER) 0))))
Merge.kif 4889-4900
If
equal
the
greatest
common divisor of @ROW and
an integer
and
equal
the integer
and 0,
then for all
another integer
if
the other integer
is a
member
of (@ROW),
then
equal
the other integer
mod
the integer
and 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 4902-4916
If
equal
the
greatest
common divisor of @ROW and
an integer
and
equal
the integer
and 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
equal
the third integer
mod
the other integer
and 0
(=>
(
and
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?NUMBER ?ELEMENT) 0))))
Merge.kif 4974-4984
If
equal
the
least
common multiple of @ROW and
an integer
and
equal
the integer
and 0,
then for all
another integer
if
the other integer
is a
member
of (@ROW),
then
equal
the integer
mod
the other integer
and 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 4986-5000
If
equal
the
least
common multiple of @ROW and
an integer
and
equal
the integer
and 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
equal
the other integer
mod
the third integer
and 0
(=>
(
and
(
equal
?LIST1 ?LIST2)
(
equal
?LIST1
(
ListFn
@ROW1))
(
equal
?LIST2
(
ListFn
@ROW2)))
(
equal
(
ListOrderFn
(
ListFn
@ROW1) ?NUMBER)
(
ListOrderFn
(
ListFn
@ROW2) ?NUMBER)))
Merge.kif 289-296
If
equal
a list
and
another list
and
equal
the list
and (@ROW1) and
equal
the other list
and (@ROW2),
then
equal
a third entity
element
of (@ROW1) and
the third entity
element
of (@ROW2)
(=>
(
and
(
equal
?R
(
SubListFn
?S ?E ?L))
(
equal
(
SubtractionFn
?E ?S) 1))
(
equal
?R
(
ListFn
(
ListOrderFn
?L ?S))))
Merge.kif 3192-3201
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 integer
th
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 3203-3215
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 integer
th
element
of
the other list
) and the sub-list from (1 and
the positive integer
) to
the integer
of
the other list
(=>
(
and
(
exactCardinality
?REL ?ARG 1)
(
instance
?REL
Predicate
)
(?REL @ARGS)
(
equal
?X
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
not
(
exists
(?Y)
(
and
(
equal
?Y
(
ListOrderFn
(
ListFn
@ARGS) ?ARG))
(
not
(
equal
?X ?Y))))))
Media.kif 2095-2105
If there can be 1
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
and
the relation
@ARGS and
equal
another entity
and
the positive integer
th
element
of (@ARGS),
then there doesn't exist
a fourth entity
such that
equal
the fourth entity
and
the positive integer
th
element
of (@ARGS) and
equal
the other entity
and
the fourth entity
(=>
(
and
(
exactCardinality
?REL ?ARG 1)
(
instance
?REL
Predicate
))
(
exists
(?X @ARGS)
(
and
(?REL @ARGS)
(
equal
?X
(
ListOrderFn
(
ListFn
@ARGS) ?ARG))
(
not
(
exists
(?Y)
(
and
(
equal
?Y
(
ListOrderFn
(
ListFn
@ARGS) ?ARG))
(
not
(
equal
?X ?Y))))))))
Media.kif 2077-2092
If there can be 1
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
,
then there exist
an entity
and @ARGS such that
the relation
@ARGS and
equal
the entity
and
the positive integer
th
element
of (@ARGS) and there doesn't exist
a fourth entity
such that
equal
the fourth entity
and
the positive integer
th
element
of (@ARGS) and
equal
the entity
and
the fourth entity
(=>
(
and
(
exactCardinality
?REL ?ARG ?COUNT)
(
instance
?REL
Predicate
))
(
exists
(?S ?EL @ARGS)
(
and
(
instance
?S
SetOrClass
)
(=>
(
and
(?REL @ARGS)
(
equal
?EL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
and
(
instance
?EL ?S)
(
equal
(
CardinalityFn
?S) ?COUNT))))))
Media.kif 2139-2152
If there can be
an integer
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
,
then there exist
a class
,
an entity
and @ARGS such that
the class
is an
instance
of
set or class
and
if
the relation
@ARGS and
equal
the entity
and
the positive integer
th
element
of (@ARGS),
then
the entity
is an
instance
of
the class
and
equal
the number of
instances
in
the class
and
the integer
(=>
(
and
(
maxCardinality
?REL ?ARG ?COUNT)
(
instance
?REL
Predicate
))
(
exists
(?S ?EL @ARGS)
(
and
(
instance
?S
SetOrClass
)
(=>
(
and
(?REL @ARGS)
(
equal
?EL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
and
(
instance
?EL ?S)
(
lessThanOrEqualTo
(
CardinalityFn
?S) ?COUNT))))))
Media.kif 2212-2225
If there can be at most
an integer
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
,
then there exist
a class
,
an entity
and @ARGS such that
the class
is an
instance
of
set or class
and
if
the relation
@ARGS and
equal
the entity
and
the positive integer
th
element
of (@ARGS),
then
the entity
is an
instance
of
the class
and the number of
instances
in
the class
is
less
than or equal to
the integer
(=>
(
and
(
minCardinality
?REL ?ARG ?COUNT)
(
instance
?REL
Predicate
))
(
exists
(?S ?EL @ARGS)
(
and
(
instance
?S
SetOrClass
)
(=>
(
and
(?REL @ARGS)
(
equal
?EL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG)))
(
and
(
instance
?EL ?S)
(
greaterThanOrEqualTo
(
CardinalityFn
?S) ?COUNT))))))
Media.kif 2176-2189
If there are at least
an integer
values
to argument
a positive integer
of
a relation
and
the relation
is an
instance
of
predicate
,
then there exist
a class
,
an entity
and @ARGS such that
the class
is an
instance
of
set or class
and
if
the relation
@ARGS and
equal
the entity
and
the positive integer
th
element
of (@ARGS),
then
the entity
is an
instance
of
the class
and the number of
instances
in
the class
is
greater
than or equal to
the integer
(=>
(
and
(
valence
?REL ?NUMBER)
(
instance
?REL
Predicate
))
(
forall
(@ROW)
(=>
(?REL @ROW)
(
equal
(
ListLengthFn
(
ListFn
@ROW)) ?NUMBER))))
Merge.kif 3061-3068
If
a relation
has
a positive integer
argument
(s) and
the relation
is an
instance
of
predicate
,
then for all @ROW
if
the relation
@ROW,
then
equal
length
of (@ROW) and
the positive integer
(=>
(
contraryAttribute
@ROW)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Attribute
)))
Merge.kif 457-461
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 2963-2968
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 2970-2979
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
equal
the third class
and
the fourth class
,
then
the third class
is
disjoint
from
the fourth class
(=>
(
disjointDecomposition
@ROW)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
instance
?ELEMENT
Class
)))
Merge.kif 567-571
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 4882-4887
If
equal
the
greatest
common divisor of @ROW and
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 4967-4972
If
equal
the
least
common multiple of @ROW and
an integer
,
then
if
another entity
is a
member
of (@ROW),
then
the other entity
is an
instance
of
number
(=>
(
exactCardinality
?REL ?ARG ?COUNT)
(
exists
(?EL @ARGS)
(
equal
(
CardinalityFn
(
KappaFn
?EL
(
and
(?REL @ARGS)
(
equal
?EL
(
ListOrderFn
(
ListFn
@ARGS) ?ARG))))) ?COUNT)))
Media.kif 2127-2136
If there can be
an integer
values
to argument
another integer
of
a relation
,
then there exist
a symbolic string
and @ARGS such that
equal
the number of
instances
in the
class
described by
the symbolic string
and
the integer
(=>
(
exhaustiveAttribute
?ATTRCLASS @ROW)
(
not
(
exists
(?EL)
(
and
(
instance
?EL ?ATTRCLASS)
(
not
(
exists
(?ATTR ?NUMBER)
(
and
(
equal
?EL ?ATTR)
(
equal
?ATTR
(
ListOrderFn
(
ListFn
@ROW) ?NUMBER)))))))))
Merge.kif 512-524
If @ROW are all the
attributes
of
another kind of attribute
,
then there doesn't exist
an entity
such that
the entity
is an
instance
of
another kind of attribute
and there don't exist
another entity
and
a positive integer
such that
equal
the entity
and
the other entity
and
equal
the other entity
and
the positive integer
th
element
of (@ROW)
(=>
(
exhaustiveAttribute
?CLASS @ROW)
(
forall
(?ATTR1)
(=>
(
instance
?ATTR1 ?CLASS)
(
exists
(?ATTR2)
(
and
(
inList
?ATTR2
(
ListFn
@ROW))
(
equal
?ATTR1 ?ATTR2))))))
Merge.kif 502-510
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
equal
the entity
and
the other entity
(=>
(
exhaustiveDecomposition
?CLASS @ROW)
(
forall
(?OBJ)
(=>
(
instance
?OBJ ?CLASS)
(
exists
(?ITEM)
(
and
(
inList
?ITEM
(
ListFn
@ROW))
(
instance
?OBJ ?ITEM))))))
Merge.kif 2953-2961
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
statement
(
forall
(@ROW ?ITEM)
(
equal
(
ListLengthFn
(
ListFn
@ROW ?ITEM))
(
SuccessorFn
(
ListLengthFn
(
ListFn
@ROW)))))
Merge.kif 3050-3053
For all @ROW and
another entity
equal
length
of (@ROW and
the other entity
) and (
length
of (@ROW)+1)
(
forall
(@ROW ?ITEM)
(
equal
(
ListOrderFn
(
ListFn
@ROW ?ITEM)
(
ListLengthFn
(
ListFn
@ROW ?ITEM))) ?ITEM))
Merge.kif 3055-3059
For all @ROW and
another entity
equal
length
of (@ROW and
the other entity
)th
element
of (@ROW and
the other entity
) and
the other entity
(
forall
(@ROW ?ITEM)
(
initialList
(
ListFn
@ROW)
(
ListFn
@ROW ?ITEM)))
Merge.kif 3330-3331
For all @ROW and
another entity
(@ROW)
start
s (@ROW and
the other entity
)
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