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
DayFn
Sigma KEE - DayFn
DayFn
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 2760-2763
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8592-8597
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 1488-1492
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8588-8588
The number 1 argument of
day
is an
instance
of
positive integer
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8589-8589
The number 2 argument of
day
is a
subclass
of
month
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8586-8586
Day
is an
instance
of
binary function
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8587-8587
Day
is an
instance
of
partial valued relation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8585-8585
Day
is an
instance
of
temporal relation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8590-8590
The values returned by
day
are
subclasses
of
day
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 469-469
No TPTP formula. May not be expressible in strict first order.
english_format.kif 475-475
No TPTP formula. May not be expressible in strict first order.
french_format.kif 271-271
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 65-65
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 2061-2061
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 223-223
No TPTP formula. May not be expressible in strict first order.
relations-cb.txt 99-99
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 277-277
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 612-612
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 106-106
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 292-292
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 298-298
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 146-146
No TPTP formula. May not be expressible in strict first order.
Merge.kif 9231-9231
Day
is
internally
related to
day
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 18660-18660
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 470-470
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 18659-18659
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 18658-18658
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 147-147
antecedent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24236-24246
If
a day
is a
birthdate
of
a human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
another kind of day
and
an integer
such that
the human
's
birthday
is
another kind of day
and
the other kind of day
is a
subclass
of
day
and
the integer
is an
instance
of
integer
and
the other kind of day
is
equal
to the
day
the positive integer
and
the integer
is
greater
than
another integer
No TPTP formula. May not be expressible in strict first order.
Government.kif 612-617
If the
day
a positive integer
is a
commemorates
date of
a kind of holiday
and
a time interval
is an
instance
of
a kind of holiday
and
another time interval
is an
instance
of the
year
an integer
,
then
the time interval
doesn't happen
earlier
than
the other time interval
No TPTP formula. May not be expressible in strict first order.
Government.kif 619-625
If the
day
a positive integer
is a
commemorates
date of
a kind of holiday
and
an entity
is an
instance
of
a kind of holiday
and
the kind of holiday
is a
subclass
of
fixed holiday
and
an integer
is
less
than or equal to
another entity
-YEAR,
then
the entity
is an
instance
of the
day
the positive integer
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23916-23932
If
menopause
is an
attribute
of
a human
holds
during
a time interval
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
and
a real number
is
equal
to (49 and
an integer
) and
another real number
is
equal
to (52 and
the integer
) and
a time point
is
equal
to the
beginning
of
the time interval
,
then the statement
the time point
is
greater
than
the real number
and
the other real number
is
greater
than
the time point
has the
modal
force
of
likely
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8722-8729
If
a time interval
is an
instance
of the
day
a positive integer
and
another time interval
is an
instance
of the
day
another positive integer
and
a time point
is
equal
to the
beginning
of
the time interval
and
another time point
is
equal
to the
beginning
of
the other time interval
and
the other positive integer
is
greater
than
the positive integer
,
then
the time point
happens
before
the other time point
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8731-8736
If
a time interval
is an
instance
of the
day
a positive integer
and
another time interval
is an
instance
of the
day
another positive integer
and
the other positive integer
is
greater
than
the positive integer
,
then
the time interval
happens
earlier
than
the other time interval
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 14837-14846
If
a time position
is an
instance
of the
day
a positive integer
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
and
the other positive integer
is
equal
to (
the positive integer
and 7)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8603-8608
If
a time interval
is an
instance
of the
day
a positive integer
and
another time interval
is an
instance
of the
day
another positive integer
and (
the other positive integer
and
the positive integer
) is
equal
to 1,
then
the time interval
meet
s
the other time interval
No TPTP formula. May not be expressible in strict first order.
Biography.kif 69-85
If
a process
is an
instance
of
BarMitzvah
and
a human
is a
patient
of
the process
and
the human
is an
instance
of
boy
and
the human
is a
member
of
a collection
and
the collection
is an
instance
of
judaism
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
the integer
is
equal
to (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
and the
time
of existence of
the process
is
equal
to immediately
after
the time position
No TPTP formula. May not be expressible in strict first order.
Biography.kif 99-115
If
a process
is an
instance
of
BatMitzvah
and
a human
is a
patient
of
the process
and
the human
is an
instance
of
girl
and
the human
is a
member
of
a collection
and
the collection
is an
instance
of
judaism
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
the integer
is
equal
to (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
and the
time
of existence of
the process
is
equal
to immediately
after
the time position
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17206-17212
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and the time
the time position
in zone
central time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
the nonnegative integer
and 6)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17218-17224
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and the time
the time position
in zone
eastern time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
the nonnegative integer
and 5)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17194-17200
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and the time
the time position
in zone
mountain time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
the nonnegative integer
and 7)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17182-17188
If
a time position
is an
instance
of the
hour
a nonnegative integer
and
another time position
is an
instance
of the
hour
another nonnegative integer
and the time
the time position
in zone
pacific time zone
is
equal
to
the other time position
,
then
the other nonnegative integer
is
equal
to (
the nonnegative integer
and 8)
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24195-24206
If
a physical
is an
instance
of
wedding
and
date
of
the physical
is
a day
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
another kind of day
and
an integer
such that
weddingAnniversary
the physical
and
another kind of day
and
the other kind of day
is a
subclass
of
day
and
the integer
is an
instance
of
integer
and
the other kind of day
is
equal
to the
day
the positive integer
and
the integer
is
greater
than
another integer
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8599-8601
If
an entity
is an
instance
of the
day
a positive integer
,
then
the positive integer
is
less
than or equal to 31
consequent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24236-24246
If
a day
is a
birthdate
of
a human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
another kind of day
and
an integer
such that
the human
's
birthday
is
another kind of day
and
the other kind of day
is a
subclass
of
day
and
the integer
is an
instance
of
integer
and
the other kind of day
is
equal
to the
day
the positive integer
and
the integer
is
greater
than
another integer
No TPTP formula. May not be expressible in strict first order.
Government.kif 619-625
If the
day
a positive integer
is a
commemorates
date of
a kind of holiday
and
an entity
is an
instance
of
a kind of holiday
and
the kind of holiday
is a
subclass
of
fixed holiday
and
an integer
is
less
than or equal to
another entity
-YEAR,
then
the entity
is an
instance
of the
day
the positive integer
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 14837-14846
If
a time position
is an
instance
of the
day
a positive integer
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
and
the other positive integer
is
equal
to (
the positive integer
and 7)
No TPTP formula. May not be expressible in strict first order.
Biography.kif 69-85
If
a process
is an
instance
of
BarMitzvah
and
a human
is a
patient
of
the process
and
the human
is an
instance
of
boy
and
the human
is a
member
of
a collection
and
the collection
is an
instance
of
judaism
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
the integer
is
equal
to (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
and the
time
of existence of
the process
is
equal
to immediately
after
the time position
No TPTP formula. May not be expressible in strict first order.
Biography.kif 99-115
If
a process
is an
instance
of
BatMitzvah
and
a human
is a
patient
of
the process
and
the human
is an
instance
of
girl
and
the human
is a
member
of
a collection
and
the collection
is an
instance
of
judaism
and
a day
is a
birthdate
of
the human
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
an integer
and
a time position
such that
the integer
is an
instance
of
integer
and
the integer
is
equal
to (
another integer
and 13) and
the time position
is an
instance
of the
day
the positive integer
and the
time
of existence of
the process
is
equal
to immediately
after
the time position
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 24195-24206
If
a physical
is an
instance
of
wedding
and
date
of
the physical
is
a day
and
the day
is an
instance
of the
day
a positive integer
,
then there exist
another kind of day
and
an integer
such that
weddingAnniversary
the physical
and
another kind of day
and
the other kind of day
is a
subclass
of
day
and
the integer
is an
instance
of
integer
and
the other kind of day
is
equal
to the
day
the positive integer
and
the integer
is
greater
than
another integer
statement
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3192-3192
The
day
1 is an
agreement
adoption date of
antarctic treaty
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3193-3193
?D is an
instance
of the
day
23 is an
agreement
effective date of
antarctic treaty
No TPTP formula. May not be expressible in strict first order.
Government.kif 2994-2994
The
day
31 is a
date
dissolved of
coordinating committee on export controls
No TPTP formula. May not be expressible in strict first order.
Government.kif 3009-3009
The
day
1 is a
date
dissolved of
council for mutual economic assistance
No TPTP formula. May not be expressible in strict first order.
Government.kif 4145-4145
The
day
25 is a
date
dissolved of
united nations preventive deployment force
No TPTP formula. May not be expressible in strict first order.
Government.kif 4285-4285
The
day
1 is a
date
dissolved of
warsaw pact
No TPTP formula. May not be expressible in strict first order.
Government.kif 2750-2750
The
day
6 is a
date
established of
african caribbean and pacific group of states
No TPTP formula. May not be expressible in strict first order.
Government.kif 2757-2757
The
day
4 is a
date
established of
african development bank
No TPTP formula. May not be expressible in strict first order.
Government.kif 2771-2771
The
day
20 is a
date
established of
agency for the french speaking community
No TPTP formula. May not be expressible in strict first order.
Government.kif 2778-2778
The
day
14 is a
date
established of
agency for the prohibition of nuclear weapons in latin america and the caribbean
No TPTP formula. May not be expressible in strict first order.
Government.kif 2796-2796
The
day
26 is a
date
established of
andean community of nations
No TPTP formula. May not be expressible in strict first order.
Government.kif 2801-2801
The
day
23 is a
date
established of
antarctic treaty council
No TPTP formula. May not be expressible in strict first order.
Government.kif 2812-2812
The
day
18 is a
date
established of
arab bank for economic development in africa
No TPTP formula. May not be expressible in strict first order.
Government.kif 2818-2818
The
day
16 is a
date
established of
arab cooperation council
No TPTP formula. May not be expressible in strict first order.
Government.kif 2824-2824
The
day
16 is a
date
established of
arab fund for economic and social development
No TPTP formula. May not be expressible in strict first order.
Government.kif 2833-2833
The
day
22 is a
date
established of
arab league
No TPTP formula. May not be expressible in strict first order.
Government.kif 2842-2842
The
day
17 is a
date
established of
arab maghreb union
No TPTP formula. May not be expressible in strict first order.
Government.kif 2851-2851
The
day
27 is a
date
established of
arab monetary fund
No TPTP formula. May not be expressible in strict first order.
Government.kif 2857-2857
The
day
7 is a
date
established of
asia pacific economic cooperation
No TPTP formula. May not be expressible in strict first order.
Government.kif 2863-2863
The
day
19 is a
date
established of
asian development bank
No TPTP formula. May not be expressible in strict first order.
Government.kif 2869-2869
The
day
8 is a
date
established of
association of southeast asian nations
No TPTP formula. May not be expressible in strict first order.
Government.kif 2889-2889
The
day
1 is a
date
established of
australia new zealand united states security treaty
No TPTP formula. May not be expressible in strict first order.
Government.kif 2895-2895
The
day
20 is a
date
established of
bank for international settlements
No TPTP formula. May not be expressible in strict first order.
Government.kif 2901-2901
The
day
3 is a
date
established of
benelux economic union
No TPTP formula. May not be expressible in strict first order.
Government.kif 2921-2921
The
day
25 is a
date
established of
black sea economic cooperation zone
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