Browsing Interface
: Welcome guest :
log in
[
Home
|
Graph
| ]
KB:
SUMO
Language:
ChineseLanguage
ChinesePinyinWriting
ChineseSimplifiedWriting
ChineseTraditionalLanguage
EnglishLanguage
FrenchLanguage
GermanLanguage
JapaneseLanguage
SpanishLanguage
SwedishLanguage
Formal Language:
OWL
SUO-KIF
TPTP
traditionalLogic
KB Term:
Term intersection
English Word:
Any
Noun
Verb
Adjective
Adverb
TemporalCompositionFn
Sigma KEE - TemporalCompositionFn
TemporalCompositionFn
appearance as argument number 1
(
documentation
TemporalCompositionFn
ChineseLanguage
"这是表示以较小的
TimeInterval
组成较大的
TimeInterval
的基本
Function
。例如：如果 ThisSeptember 是
September
的一个
instance
， 那么(
TemporalCompositionFn
ThisSeptember
Day
)表示构成 ThisSeptember 内连续日数的
Class
。注：我们可以用函数
CardinalityFn
来得出这个
Class
实例的数目。")
chinese_format.kif 2819-2822
(
documentation
TemporalCompositionFn
EnglishLanguage
"The basic
Function
for expressing the composition of larger
TimeInterval
s out of smaller
TimeInterval
s. For example, if ThisSeptember is an
instance
of
September
, (
TemporalCompositionFn
ThisSeptember
Day
) denotes the
Class
of consecutive days that make up ThisSeptember. Note that one can obtain the number of instances of this
Class
by using the function
CardinalityFn
.")
Merge.kif 9274-9279
(
domain
TemporalCompositionFn
1
TimeInterval
)
Merge.kif 9271-9271
The number 1 argument of
temporal composition
is an
instance
of
time interval
(
domainSubclass
TemporalCompositionFn
2
TimeInterval
)
Merge.kif 9272-9272
The number 2 argument of
temporal composition
is a
subclass
of
time interval
(
instance
TemporalCompositionFn
BinaryFunction
)
Merge.kif 9269-9269
Temporal composition
is an
instance
of
binary function
(
instance
TemporalCompositionFn
TemporalRelation
)
Merge.kif 9268-9268
Temporal composition
is an
instance
of
temporal relation
(
instance
TemporalCompositionFn
TotalValuedRelation
)
Merge.kif 9270-9270
Temporal composition
is an
instance
of
total valued relation
(
rangeSubclass
TemporalCompositionFn
TimeInterval
)
Merge.kif 9273-9273
The values returned by
temporal composition
are
subclasses
of
time interval
appearance as argument number 2
(
format
ChineseLanguage
TemporalCompositionFn
"分拆 %1 为 %3 的 %2")
chinese_format.kif 447-447
(
format
EnglishLanguage
TemporalCompositionFn
"decomposition of %1 into %3 %2s")
english_format.kif 453-453
(
termFormat
ChineseLanguage
TemporalCompositionFn
"时间分拆函数")
chinese_format.kif 448-448
(
termFormat
ChineseLanguage
TemporalCompositionFn
"时间构成")
domainEnglishFormat.kif 57401-57401
(
termFormat
ChineseTraditionalLanguage
TemporalCompositionFn
"時間構成")
domainEnglishFormat.kif 57400-57400
(
termFormat
EnglishLanguage
TemporalCompositionFn
"temporal composition")
domainEnglishFormat.kif 57399-57399
antecedent
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
exists
(?TIME)
(
and
(
instance
?TIME ?CLASS)
(
finishes
?TIME ?INTERVAL))))
Merge.kif 9314-9319
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then there exists
a third time interval
such that
the third time interval
is an
instance
of
another kind of time interval
and
the third time interval
finish
es
the time interval
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
exists
(?TIME)
(
and
(
instance
?TIME ?CLASS)
(
starts
?TIME ?INTERVAL))))
Merge.kif 9307-9312
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then there exists
a third time interval
such that
the third time interval
is an
instance
of
another kind of time interval
and
the third time interval
start
s
the time interval
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME)
(=>
(
and
(
instance
?TIME
TimePoint
)
(
temporalPart
?TIME ?INTERVAL))
(
exists
(?INSTANCE)
(
and
(
instance
?INSTANCE ?CLASS)
(
temporalPart
?TIME ?INSTANCE))))))
Merge.kif 9345-9355
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a time position
if
the time position
is an
instance
of
time point
and
the time position
is a
part
of
the time interval
,
then there exists
another time position
such that
the other time position
is an
instance
of
another kind of time interval
and
the time position
is a
part
of
the other time position
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1 ?TIME2)
(=>
(
and
(
instance
?TIME1 ?CLASS)
(
instance
?TIME2 ?CLASS)
(
not
(
equal
?TIME1 ?TIME2)))
(
or
(
meetsTemporally
?TIME1 ?TIME2)
(
meetsTemporally
?TIME2 ?TIME1)
(
earlier
?TIME1 ?TIME2)
(
earlier
?TIME2 ?TIME1)))))
Merge.kif 9293-9305
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
and
a fourth time interval
if
the third time interval
is an
instance
of
another kind of time interval
and
the fourth time interval
is an
instance
of
the other kind of time interval
and
the third time interval
is not
equal
to
the fourth time interval
,
then
the third time interval
meet
s
the fourth time interval
or
the fourth time interval
meet
s
the third time interval
or
the third time interval
happens
earlier
than
the fourth time interval
or
the fourth time interval
happens
earlier
than
the third time interval
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1 ?TIME2)
(=>
(
and
(
instance
?TIME1 ?INTERVALTYPE)
(
instance
?TIME2 ?CLASS))
(
exists
(?DURATION)
(
and
(
duration
?TIME1 ?DURATION)
(
duration
?TIME2 ?DURATION))))))
Merge.kif 9281-9291
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
and
a fourth time interval
if
the third time interval
is an
instance
of
the time interval
TYPE and
the fourth time interval
is an
instance
of
another kind of time interval
,
then there exists
a time duration
such that
duration
of
the third time interval
is
the time duration
and
duration
of
the fourth time interval
is
the time duration
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1)
(=>
(
and
(
instance
?TIME1 ?CLASS)
(
not
(
finishes
?TIME1 ?INTERVAL)))
(
exists
(?TIME2)
(
and
(
instance
?TIME2 ?CLASS)
(
meetsTemporally
?TIME1 ?TIME2))))))
Merge.kif 9321-9331
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
if
the third time interval
is an
instance
of
another kind of time interval
and
the third time interval
doesn't
finish
the time interval
,
then there exists
a fourth time interval
such that
the fourth time interval
is an
instance
of
the other kind of time interval
and
the third time interval
meet
s
the fourth time interval
(=>
(
equal
(
TemporalCompositionFn
?INTERVAL ?INTERVALTYPE) ?CLASS)
(
forall
(?TIME1)
(=>
(
and
(
instance
?TIME1 ?CLASS)
(
not
(
starts
?TIME1 ?INTERVAL)))
(
exists
(?TIME2)
(
and
(
instance
?TIME2 ?CLASS)
(
meetsTemporally
?TIME2 ?TIME1))))))
Merge.kif 9333-9343
If
decomposition
of
a time interval
into
the time interval
TYPEs is
equal
to
another kind of time interval
,
then for all
a third time interval
if
the third time interval
is an
instance
of
another kind of time interval
and
the third time interval
doesn't
start
the time interval
,
then there exists
a fourth time interval
such that
the fourth time interval
is an
instance
of
the other kind of time interval
and
the fourth time interval
meet
s
the third time interval
consequent
(=>
(
and
(
instance
?MONTH
Month
)
(
duration
?MONTH
(
MeasureFn
?NUMBER
DayDuration
)))
(
equal
(
CardinalityFn
(
TemporalCompositionFn
?MONTH
Day
)) ?NUMBER))
Merge.kif 9361-9365
If
a time interval
is an
instance
of
month
and
duration
of
the time interval
is
an integer
day duration
(s),
then the number of
instances
in
decomposition
of
the time interval
into
day
s is
equal
to
the integer
(=>
(
instance
?DAY
Day
)
(
equal
(
CardinalityFn
(
TemporalCompositionFn
?DAY
Hour
)) 24))
Merge.kif 9371-9373
If
a time interval
is an
instance
of
day
,
then the number of
instances
in
decomposition
of
the time interval
into
hour
s is
equal
to 24
(=>
(
instance
?HOUR
Hour
)
(
equal
(
CardinalityFn
(
TemporalCompositionFn
?HOUR
Minute
)) 60))
Merge.kif 9375-9377
If
a time interval
is an
instance
of
hour
,
then the number of
instances
in
decomposition
of
the time interval
into
minute
s is
equal
to 60
(=>
(
instance
?MINUTE
Minute
)
(
equal
(
CardinalityFn
(
TemporalCompositionFn
?MINUTE
Second
)) 60))
Merge.kif 9379-9381
If
a time interval
is an
instance
of
minute
,
then the number of
instances
in
decomposition
of
the time interval
into
second
s is
equal
to 60
(=>
(
instance
?WEEK
Week
)
(
equal
(
CardinalityFn
(
TemporalCompositionFn
?WEEK
Day
)) 7))
Merge.kif 9367-9369
If
a time interval
is an
instance
of
week
,
then the number of
instances
in
decomposition
of
the time interval
into
day
s is
equal
to 7
(=>
(
instance
?YEAR
Year
)
(
equal
(
CardinalityFn
(
TemporalCompositionFn
?YEAR
Month
)) 12))
Merge.kif 9357-9359
If
a time interval
is an
instance
of
year
,
then the number of
instances
in
decomposition
of
the time interval
into
month
s is
equal
to 12
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
