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
holdsDuring
Sigma KEE - holdsDuring
holdsDuring
appearance as argument number 1
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 2083-2085
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3884-3887
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 731-733
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3881-3881
域
持有期間
, 1 and
TimePosition
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3882-3882
域
持有期間
, 2 and
Formula
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3880-3880
例
持有期間
and
AsymmetricRelation
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3879-3879
例
持有期間
and
BinaryPredicate
appearance as argument number 2
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 121-121
No TPTP formula. May not be expressible in strict first order.
english_format.kif 122-122
No TPTP formula. May not be expressible in strict first order.
french_format.kif 82-82
No TPTP formula. May not be expressible in strict first order.
relations-it.txt 129-129
No TPTP formula. May not be expressible in strict first order.
japanese_format.kif 1909-1909
No TPTP formula. May not be expressible in strict first order.
portuguese_format.kif 34-34
No TPTP formula. May not be expressible in strict first order.
relations-cz.txt 117-117
No TPTP formula. May not be expressible in strict first order.
relations-de.txt 142-142
No TPTP formula. May not be expressible in strict first order.
relations-hindi.txt 169-169
No TPTP formula. May not be expressible in strict first order.
relations-ro.kif 101-101
No TPTP formula. May not be expressible in strict first order.
relations-sv.txt 81-81
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 264-264
No TPTP formula. May not be expressible in strict first order.
Merge.kif 3869-3869
相關的內部概念
時間
and
持有期間
No TPTP formula. May not be expressible in strict first order.
chinese_format.kif 122-122
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 28353-28353
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 28352-28352
No TPTP formula. May not be expressible in strict first order.
domainEnglishFormat.kif 28351-28351
No TPTP formula. May not be expressible in strict first order.
terms-de.txt 42-42
No TPTP formula. May not be expressible in strict first order.
relations-tg.txt 265-265
antecedent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30178-30188
例
Entity
and
BodyPart
持有期間
TimePosition
and
attribute
Entity
and
Bare
持有期間
TimePosition
and
entity
例
entity
and
Clothing
covers
entity
and
Entity
No TPTP formula. May not be expressible in strict first order.
Weather.kif 2680-2690
例
Entity
and
Region
持有期間
TimePosition
and
屬性
Entity
and
StandardAmbientTemperaturePressure
持有期間
TimePosition
and
測量
298.15 and
凱文度
是
Entity
的
air
溫度
測量
29.530 and
英寸汞
是
Entity
的
barometric
壓力
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17254-17262
持有期間
TimePosition
and
例
entity
and
Human
entity
採用
entity
and
entity
持有期間
TimePosition
and
attribute
entity
and
失業的
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30132-30140
持有期間
TimePosition
and
attribute
entity
and
Barefoot
持有期間
TimePosition
and
entity
例
entity
and
鞋
穿
entity
and
entity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30145-30153
持有期間
TimePosition
and
attribute
entity
and
Naked
持有期間
TimePosition
and
entity
例
entity
and
Clothing
穿
entity
and
entity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30223-30236
持有期間
TimeInterval
and
attribute
Entity
and
Alone
Entity
2
Process
等於
Entity
and
Entity
2
例
Entity
2 and
AutonomousAgent
例
Process
and
SocialInteraction
期間
何時
Process
and
TimeInterval
Entity
是事件
Process
的
involved
Entity
2 是事件
Process
的
involved
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30271-30279
持有期間
TimeInterval
and
attribute
AutonomousAgent
and
Mute
Process
例
Process
and
說話
期間
何時
Process
and
TimeInterval
agent
Process
and
AutonomousAgent
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1601-1607
持有期間
TimePosition
and
attribute
entity
and
LegalAgent
持有期間
TimePosition
and
能力
LegalAction
,
agent
and
entity
能力
LegalAction
,
患者
and
entity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 6231-6244
allergic
Human
and
Substance
例
Substance
UB and
Substance
持有期間
TimePosition
and
空間的符合
Substance
UB and
Human
模態屬性
entity
例
entity
and
AllergicReaction
體驗者
entity
and
Human
暫時重疊
TimePosition
and
何時
entity
之前
開始
TimePosition
and
開始
何時
entity
and
容易
No TPTP formula. May not be expressible in strict first order.
Merge.kif 13841-13854
測量
RealNumber
and
UnitOfMeasure
是
PureSubstance
的
boiling
點
例
Entity
and
PureSubstance
持有期間
TimeInterval
and
測量
Entity
and
測量
RealNumber
and
UnitOfMeasure
例
UnitOfMeasure
and
UnitOfTemperature
大於或等於
RealNumber
and
RealNumber
持有期間
TimeInterval
and
attribute
Entity
and
加油站
Process
暫時重疊
何時
Process
and
TimeInterval
例
Process
and
Boiling
患者
Process
and
Entity
No TPTP formula. May not be expressible in strict first order.
Medicine.kif 367-385
breathingRate
AutonomousAgent
,
TimeInterval
and
Integer
例
TimeInterval
and
Minute
Integer
例
Integer
and
RecreationOrExercise
agent
Integer
and
AutonomousAgent
期間
TimeInterval
and
何時
Integer
持有期間
TimeInterval
and
attribute
AutonomousAgent
and
人類成人
比較多
Integer
and 16
少於
Integer
and 12
持有期間
TimeInterval
and
attribute
AutonomousAgent
and
Healthy
No TPTP formula. May not be expressible in strict first order.
Geography.kif 1597-1603
極地型F氣候區
是
GeographicArea
地區的
climate
類別
例
TimePosition
and
TimePosition
持有期間
TimePosition
and
測量
entity
and
攝氏度
是
GeographicArea
的
air
溫度
持有期間
TimePosition
and
比較多
10.0 and
entity
No TPTP formula. May not be expressible in strict first order.
Cars.kif 809-825
dampingRatio
物理系統
and
RealNumber
比較多
RealNumber
and 0
例
TimeInterval
and
震
患者
TimeInterval
and
物理系統
例
Entity
and
UnitOfLength
持有期間
TimeInterval
and
physicalAmplitude
TimeInterval
and
測量
RealNumber
and
Entity
持有期間
TimeInterval
and
physicalAmplitude
TimeInterval
and
測量
RealNumber
and
Entity
期間
TimeInterval
and
TimeInterval
期間
TimeInterval
and
TimeInterval
早期
TimeInterval
and
TimeInterval
比較多
RealNumber
and
RealNumber
No TPTP formula. May not be expressible in strict first order.
Cars.kif 2585-2603
engineIdleSpeed
內燃機
and
RotationFn
測量
RealNumber
and
MilesPerHour
and
TimeDuration
例
Object
and
汽車
例
Process
and
GasPedal
例
Process
and
Pushing
目的地
Process
and
Object
部分
內燃機
and
Object
部分
Object
and
Object
例
Object
and
Crankshaft
部分
Object
and
內燃機
持有期間
何時
Process
and
測量
Object
and
RotationFn
測量
entity
and
MilesPerHour
and
TimeDuration
模態屬性
比較多
entity
and
RealNumber
and
容易
No TPTP formula. May not be expressible in strict first order.
Government.kif 223-234
%2 是 1% 的
government
類別
例
Organism
and
Human
例
Organism
and
Human
持有期間
TimeInterval
and
AutonomousAgent
州
entity
的
chief
對於
Organism
家庭關係
Organism
and
Organism
早期
TimeInterval
and
TimeInterval
模態屬性
持有期間
TimeInterval
and
AutonomousAgent
州
entity
的
chief
對於
Organism
and
可能性
No TPTP formula. May not be expressible in strict first order.
Media.kif 406-411
持有期間
假日
and
attribute
CognitiveAgent
and
基督教
例
假日
and
ChristmasDay
CognitiveAgent
observes
假日
No TPTP formula. May not be expressible in strict first order.
Media.kif 509-514
持有期間
假日
and
attribute
CognitiveAgent
and
基督教
例
假日
and
EasterSunday
CognitiveAgent
observes
假日
No TPTP formula. May not be expressible in strict first order.
Merge.kif 7960-7967
持有期間
TimePosition
and
entity
Physical
and
Physical
例
Physical
and
Physical
例
Physical
and
Physical
時間
Physical
and
TimePosition
時間
Physical
and
TimePosition
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1838-1860
持有期間
TimePosition
and
attribute
Object
and
LateralRecumbant
方位
Object
,
Object
and
上
例
Object
and
LeftArm
部分
Object
and
Object
例
Object
and
RightArm
部分
Object
and
Object
例
Object
and
LeftLeg
部分
Object
and
Object
例
Object
and
RightLeg
部分
Object
and
Object
空間的符合
Object
and
Object
空間的符合
Object
and
Object
持有期間
TimePosition
and
空間的符合
Object
and
Object
空間的符合
Object
and
Object
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1862-1884
持有期間
TimePosition
and
attribute
Object
and
LateralRecumbant
方位
Object
,
Object
and
上
例
Object
and
LeftArm
部分
Object
and
Object
例
Object
and
RightArm
部分
Object
and
Object
例
Object
and
LeftLeg
部分
Object
and
Object
例
Object
and
RightLeg
部分
Object
and
Object
空間的符合
Object
and
Object
空間的符合
Object
and
Object
持有期間
TimePosition
and
空間的符合
Object
and
Object
空間的符合
Object
and
Object
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1799-1807
持有期間
TimePosition
and
attribute
Object
and
Prone
方位
Object
,
Object
and
上
例
Object
and
Chest
部分
Object
and
Object
空間的符合
Object
and
Object
No TPTP formula. May not be expressible in strict first order.
Anatomy.kif 1814-1821
持有期間
TimePosition
and
attribute
SelfConnectedObject
and
Supine
方位
SelfConnectedObject
,
Object
and
上
等於
SelfConnectedObject
and
背部
SelfConnectedObject
空間的符合
SelfConnectedObject
and
Object
No TPTP formula. May not be expressible in strict first order.
emotion.kif 161-172
持有期間
TimePosition
and
attribute
entity
and
EmotionalState
actionTendency
EmotionalState
and
EmotionalBehavioralProcess
模態屬性
entity
例
entity
and
EmotionalBehavioralProcess
期間
何時
entity
and
TimePosition
體驗者
entity
and
entity
and
容易
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 23916-23932
持有期間
TimeInterval
and
attribute
Human
and
Menopausal
Day
是
Human
的
birthdate
例
Day
and
天
PositiveInteger
and
月
Month
and
年
Integer
等於
RealNumber
and
加成
49 and
Integer
等於
RealNumber
and
加成
52 and
Integer
等於
TimePoint
and
開始
TimeInterval
模態屬性
比較多
TimePoint
and
RealNumber
比較多
RealNumber
and
TimePoint
and
容易
No TPTP formula. May not be expressible in strict first order.
Merge.kif 18246-18254
持有期間
TimePosition
and
attribute
Object
and
DeadOrMissingBodyPartFn
Class
例
Class
I and
Class
部分
Class
I and
Object
有目的
Class
I and
Formula
Formula
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
consequent
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30178-30188
例
Entity
and
BodyPart
持有期間
TimePosition
and
attribute
Entity
and
Bare
持有期間
TimePosition
and
entity
例
entity
and
Clothing
covers
entity
and
Entity
No TPTP formula. May not be expressible in strict first order.
Merge.kif 12466-12473
例
Process
and
Combining
資源
Process
and
Object
結果
Process
and
Entity
持有期間
開始
何時
Process
and
部分
Object
and
Entity
持有期間
結束
何時
Process
and
部分
Object
and
Entity
No TPTP formula. May not be expressible in strict first order.
Weather.kif 2680-2690
例
Entity
and
Region
持有期間
TimePosition
and
屬性
Entity
and
StandardAmbientTemperaturePressure
持有期間
TimePosition
and
測量
298.15 and
凱文度
是
Entity
的
air
溫度
測量
29.530 and
英寸汞
是
Entity
的
barometric
壓力
No TPTP formula. May not be expressible in strict first order.
People.kif 357-390
例
年
and
年
年
EAR
等於
GeopoliticalArea
和
年
的
male
出生估計壽命 and
RealNumber
List
Integer
,
SymbolicString
,
entity
,
entity
and
entity
例
List
and
List
例
列表長度
List
and
Integer
List
ITEM
在列表中
List
ITEM and
List
例
List
ITEM and
SymbolicString
Entity
例
Entity
and
SymbolicString
在列表中
Entity
and
List
等於
Integer
and
基數
卡帕
SymbolicString
and
例
entity
and
Birth
體驗者
entity
and
entity
例
entity
and
Human
attribute
entity
and
男
期間
何時
entity
and
年
等於
哪裡
entity
and
何時
entity
and
GeopoliticalArea
例
entity
and
Death
體驗者
entity
and
entity
持有期間
何時
entity
and
年齡
entity
and
測量
SymbolicString
and
年持續時間
RealNumber
是
List
的
average
No TPTP formula. May not be expressible in strict first order.
People.kif 403-436
例
年
and
年
Integer
等於
GeopoliticalArea
和
年
的
female
出生預期壽命 and
RealNumber
List
Integer
,
SymbolicString
,
entity
,
entity
and
entity
例
List
and
List
例
列表長度
List
and
Integer
List
ITEM
在列表中
List
ITEM and
List
例
List
ITEM and
SymbolicString
Entity
例
Entity
and
SymbolicString
在列表中
Entity
and
List
等於
Integer
and
基數
卡帕
SymbolicString
and
例
entity
and
Birth
體驗者
entity
and
entity
例
entity
and
Human
attribute
entity
and
女
期間
何時
entity
and
年
等於
哪裡
entity
and
何時
entity
and
GeopoliticalArea
例
entity
and
Death
體驗者
entity
and
entity
持有期間
何時
entity
and
年齡
entity
and
測量
SymbolicString
and
年持續時間
RealNumber
是
List
的
average
No TPTP formula. May not be expressible in strict first order.
People.kif 310-342
例
年
and
年
Integer
等於
GeopoliticalArea
和
年
的出生預期
life
and
RealNumber
List
Integer
,
SymbolicString
,
entity
,
entity
and
entity
例
List
and
List
例
列表長度
List
and
Integer
List
ITEM
在列表中
List
ITEM and
List
例
List
ITEM and
SymbolicString
Entity
例
Entity
and
SymbolicString
在列表中
Entity
and
List
等於
Integer
and
基數
卡帕
SymbolicString
and
例
entity
and
Birth
體驗者
entity
and
entity
例
entity
and
Human
期間
何時
entity
and
年
等於
哪裡
entity
and
何時
entity
and
GeopoliticalArea
例
entity
and
Death
體驗者
entity
and
entity
持有期間
何時
entity
and
年齡
entity
and
測量
SymbolicString
and
年持續時間
RealNumber
是
List
的
average
No TPTP formula. May not be expressible in strict first order.
People.kif 156-187
例
年
and
年
Integer
等於
GeopoliticalArea
和
年
每一千的
migrants
and
RealNumber
等於
減法
Integer
and
Integer
and 1
例
Entity
and
年
Integer
持有期間
年
and
等於
GeopoliticalArea
的
population
and
RealNumber
等於
部
RealNumber
and 1000 and
RealNumber
等於
Integer
and
基數
卡帕
SymbolicString
and
例
SymbolicString
and
Human
持有期間
Entity
and
棲息
SymbolicString
and
GeopoliticalArea
持有期間
年
and
棲息
SymbolicString
and
GeopoliticalArea
等於
Integer
and
基數
卡帕
SymbolicString
and
例
SymbolicString
and
Human
持有期間
Entity
and
棲息
SymbolicString
and
GeopoliticalArea
持有期間
年
and
棲息
SymbolicString
and
GeopoliticalArea
等於
減法
Integer
and
Integer
and
RealNumber
等於
部
RealNumber
and
RealNumber
and
RealNumber
No TPTP formula. May not be expressible in strict first order.
People.kif 52-64
例
年
and
年
Integer
等於
GeopoliticalArea
和
年
的
population
成長 and
RealNumber
等於
減法
Integer
and
Integer
P and 1
例
TimePosition
and
年
Integer
P
持有期間
年
and
等於
GeopoliticalArea
的
population
and
RealNumber
持有期間
TimePosition
and
等於
GeopoliticalArea
的
population
and
RealNumber
等於
部
RealNumber
and
RealNumber
and
RealNumber
等於
減法
RealNumber
and 1 and
RealNumber
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1517-1522
GeopoliticalArea
對於
TimeInterval
在週期
CurrencyMeasure
的
annual
地區消費
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
GeopoliticalArea
在
annual
地區消費
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1488-1493
GeopoliticalArea
annual
對於
TimeInterval
在週期
CurrencyMeasure
的地區收入
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
GeopoliticalArea
的
annual
地區收入
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1565-1570
GeopoliticalArea
在週期
CurrencyMeasure
對於
TimeInterval
的
capital
地區支出
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
GeopoliticalArea
的
capital
地區支出
No TPTP formula. May not be expressible in strict first order.
Economy.kif 3661-3666
TimeInterval
是
CurrencyMeasure
的
currency
交換 每美元
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
美國美元
的
currency
交換匯率
No TPTP formula. May not be expressible in strict first order.
Economy.kif 3668-3673
UnitOfCurrency
對於
TimeInterval
在週期
CurrencyMeasure
的
currency
交換匯率
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
UnitOfCurrency
的
currency
交換匯率
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2819-2824
GeopoliticalArea
是 對於
TimeInterval
在期間
CurrencyMeasure
的
economic
間贈補助
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
GeopoliticalArea
的
economic
捐贈補助
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2859-2864
GeopoliticalArea
是 對於
TimeInterval
在期間
CurrencyMeasure
總共收到的
economic
補助
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
GeopoliticalArea
總共收到的
economic
補助
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2056-2061
GeopoliticalArea
是 對於
RealNumber
和
TimeInterval
在週期
發電
從來源的
electricity
分支
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
GeopoliticalArea
is 對於
RealNumber
從來源
發電
的
electricity
分支
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2549-2554
GeopoliticalArea
對
PositiveRealNumber
和
TimeInterval
在週期
GeopoliticalArea
由部分
export
夥伴
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
GeopoliticalArea
對於
PositiveRealNumber
由部分
GeopoliticalArea
export
夥伴
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2511-2516
GeopoliticalArea
對
PositiveInteger
和
TimeInterval
在週期
GeopoliticalArea
由階級
export
夥伴
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
GeopoliticalArea
對於
PositiveInteger
由階級
GeopoliticalArea
export
夥伴
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2387-2392
AutonomousAgent
對於
TimeInterval
在週期
AutonomousAgent
export
夥伴
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
AutonomousAgent
是
AutonomousAgent
的
export
夥伴
No TPTP formula. May not be expressible in strict first order.
Economy.kif 2775-2780
GeopoliticalArea
是 對於
TimeInterval
在週期
CurrencyMeasure
的
external
債務
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
CurrencyMeasure
是
GeopoliticalArea
的
external
債務
No TPTP formula. May not be expressible in strict first order.
Economy.kif 1279-1284
RealNumber
是對於
GeopoliticalArea
在週期
RealNumber
的
highest
平分家庭收入
TimePosition
例
TimePosition
and
TimeInterval
持有期間
TimePosition
and
RealNumber
是
GeopoliticalArea
的
highest
平分家庭收入
No TPTP formula. May not be expressible in strict first order.
Merge.kif 17254-17262
持有期間
TimePosition
and
例
entity
and
Human
entity
採用
entity
and
entity
持有期間
TimePosition
and
attribute
entity
and
失業的
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30132-30140
持有期間
TimePosition
and
attribute
entity
and
Barefoot
持有期間
TimePosition
and
entity
例
entity
and
鞋
穿
entity
and
entity
No TPTP formula. May not be expressible in strict first order.
Mid-level-ontology.kif 30145-30153
持有期間
TimePosition
and
attribute
entity
and
Naked
持有期間
TimePosition
and
entity
例
entity
and
Clothing
穿
entity
and
entity
No TPTP formula. May not be expressible in strict first order.
Merge.kif 1601-1607
持有期間
TimePosition
and
attribute
entity
and
LegalAgent
持有期間
TimePosition
and
能力
LegalAction
,
agent
and
entity
能力
LegalAction
,
患者
and
entity
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
statement
No TPTP formula. May not be expressible in strict first order.
People.kif 456-469
例
年
and
年
Integer
等於
GeopoliticalArea
和
年
每個女人生的
children
and
基數
卡帕
SymbolicString
and
例
entity
and
Birth
體驗者
entity
and
SymbolicString
agent
entity
and
entity
例
entity
and
Human
attribute
entity
and
女
持有期間
年
and
棲息
entity
and
GeopoliticalArea
No TPTP formula. May not be expressible in strict first order.
Military.kif 933-946
等於
GeopoliticalArea
和
年
每年的
reaching
軍事男性年齡 and
基數
卡帕
SymbolicString
and
例
SymbolicString
and
Human
attribute
SymbolicString
and
男
entity
是
GeopoliticalArea
的
military
年紀
等於
entity
and
減法
entity
and 1
持有期間
年
and
年齡
SymbolicString
and
entity
年齡
SymbolicString
and
entity
等於
entity
and
entity
棲息
SymbolicString
and
GeopoliticalArea
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2453-2457
TimePosition
例
TimePosition
and
年
1976
持有期間
TimePosition
and
斯蒂夫·沃茲尼亞克
是
史蒂芬·賈伯斯
的
coworker
No TPTP formula. May not be expressible in strict first order.
ComputingBrands.kif 2441-2445
TimePosition
例
TimePosition
and
年
2002
持有期間
TimePosition
and
提姆·庫克
是
史蒂芬·賈伯斯
的
coworker
No TPTP formula. May not be expressible in strict first order.
Media.kif 1970-1978
TimeInterval
例
TimeInterval
and
TimeInterval
飾面
TimeInterval
and
何時
JesusOfNazareth
啟動
TimeInterval
and
何時
TwelveApostles
entity
持有期間
TimeInterval
and
會員
entity
and
TwelveApostles
持有期間
TimeInterval
and
entity
是
JesusOfNazareth
的
friend
appearance as argument number 0
No TPTP formula. May not be expressible in strict first order.
Media.kif 2501-2504
持有期間
未來
TimePosition
and
例
Serbia
and
歐洲國家
例
TimePosition
and
天
5 and
月
June
and
年
2006
No TPTP formula. May not be expressible in strict first order.
Media.kif 2496-2499
持有期間
未來
TimePosition
and
例
Serbia
and
獨立國家
例
TimePosition
and
天
5 and
月
June
and
年
2006
No TPTP formula. May not be expressible in strict first order.
Media.kif 2506-2509
持有期間
未來
TimePosition
and
名
"Republic of Serbia" and
Serbia
例
TimePosition
and
天
5 and
月
June
and
年
2006
No TPTP formula. May not be expressible in strict first order.
Media.kif 2528-2531
持有期間
未來
TimePosition
and
例
TimePosition
and
天
3 and
月
June
and
年
2006
例
Montenegro
and
歐洲國家
No TPTP formula. May not be expressible in strict first order.
Media.kif 2523-2526
持有期間
未來
TimePosition
and
例
TimePosition
and
天
3 and
月
June
and
年
2006
例
Montenegro
and
獨立國家
No TPTP formula. May not be expressible in strict first order.
Media.kif 2533-2536
持有期間
未來
TimePosition
and
例
TimePosition
and
天
3 and
月
June
and
年
2006
名
"Montenegro" and
Montenegro
No TPTP formula. May not be expressible in strict first order.
Media.kif 2546-2550
持有期間
未來
TimePosition
and
例
TimePosition
and
天
3 and
月
June
and
年
2006
例
塞爾維亞和黑山
and
獨立國家
No TPTP formula. May not be expressible in strict first order.
Government.kif 2791-2794
持有期間
眼前的未來
TimePosition
and
例
TimePosition
and
天
1 and
月
October
and
年
1992
安第斯國際社會
是 "Andean Community of Nations" 的
conventional
全名
No TPTP formula. May not be expressible in strict first order.
Government.kif 2765-2769
持有期間
眼前的未來
TimePosition
and
例
TimePosition
and
年
1996
法語社區的代理機構
是 "Agency for the French-Speaking Community" 的
conventional
全名
No TPTP formula. May not be expressible in strict first order.
Media.kif 1920-1920
持有期間
何時
JesusOfNazareth
and
位於
JesusOfNazareth
and
巴勒斯坦
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