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
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 8494-8499
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8490-8490
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 8491-8491
The number 2 argument of
day
is a
subclass
of
month
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8488-8488
Day
is an
instance
of
binary function
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8489-8489
Day
is an
instance
of
partial valued relation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8487-8487
Day
is an
instance
of
temporal relation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8492-8492
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.
Merge.kif 9129-9129
Day
is
internally
related to
day
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 18651-18651
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 18650-18650
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 18649-18649
antecedent
No TPTP formula. May not be expressible in strict first order.
Government.kif 598-603
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 605-611
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 14278-14290
If
a kind of day
is
equal
to
WeekBeforeFn
the
day
a positive integer
and
a kind of day
is
equal
to the
day
the positive integer
2,
then
the positive integer
2 is
equal
to (
the positive integer
and 7)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8624-8631
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 8633-8638
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.
Merge.kif 8505-8510
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.
Merge.kif 16934-16946
If the time the
hour
a nonnegative integer
in zone
central time zone
is
equal
to the
hour
another nonnegative integer
,
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 16952-16964
If the time the
hour
a nonnegative integer
in zone
eastern time zone
is
equal
to the
hour
another nonnegative integer
,
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 16916-16928
If the time the
hour
a nonnegative integer
in zone
mountain time zone
is
equal
to the
hour
another nonnegative integer
,
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 16898-16910
If the time the
hour
a nonnegative integer
in zone
pacific time zone
is
equal
to the
hour
another nonnegative integer
,
then
the other nonnegative integer
is
equal
to (
the nonnegative integer
and 8)
No TPTP formula. May not be expressible in strict first order.
Merge.kif 8501-8503
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.
Government.kif 605-611
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
statement
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3114-3114
The
day
1 is an
agreement
adoption date of
antarctic treaty
No TPTP formula. May not be expressible in strict first order.
Geography.kif 3115-3115
The
day
23 is an
agreement
effective date of
antarctic treaty
No TPTP formula. May not be expressible in strict first order.
Government.kif 2974-2974
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 2989-2989
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 4125-4125
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 4265-4265
The
day
1 is a
date
dissolved of
warsaw pact
No TPTP formula. May not be expressible in strict first order.
Government.kif 2735-2735
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 2742-2742
The
day
4 is a
date
established of
african development bank
No TPTP formula. May not be expressible in strict first order.
Government.kif 2751-2751
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 2758-2758
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 2776-2776
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 2781-2781
The
day
23 is a
date
established of
antarctic treaty council
No TPTP formula. May not be expressible in strict first order.
Government.kif 2792-2792
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 2798-2798
The
day
16 is a
date
established of
arab cooperation council
No TPTP formula. May not be expressible in strict first order.
Government.kif 2804-2804
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 2813-2813
The
day
22 is a
date
established of
arab league
No TPTP formula. May not be expressible in strict first order.
Government.kif 2822-2822
The
day
17 is a
date
established of
arab maghreb union
No TPTP formula. May not be expressible in strict first order.
Government.kif 2831-2831
The
day
27 is a
date
established of
arab monetary fund
No TPTP formula. May not be expressible in strict first order.
Government.kif 2837-2837
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 2843-2843
The
day
19 is a
date
established of
asian development bank
No TPTP formula. May not be expressible in strict first order.
Government.kif 2849-2849
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 2869-2869
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 2875-2875
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 2881-2881
The
day
3 is a
date
established of
benelux economic union
No TPTP formula. May not be expressible in strict first order.
Government.kif 2901-2901
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