| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1380-1385 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 211-219 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 38-44 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 40-48 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 208-208 | 定义域 的 1 数量 是 关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 209-209 | 定义域 的 2 数量 是 正整数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 210-210 | 定义域 的 3 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 207-207 | 定义域 是 三元谓语 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 291-291 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 296-296 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 168-168 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 82-82 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1988-1988 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 120-120 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 177-177 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 378-378 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 122-122 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 188-188 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 175-175 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 116-116 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20112-20112 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 292-292 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20111-20111 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20110-20110 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 180-180 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31288-31295 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2985-2990 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 221-227 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 419-424 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16840-16844 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 186-190 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 186-190 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3362-3372 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3405-3415 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3425-3435 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3431-3431 | ABPFn 的 1 数量 是 群体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3476-3476 | ASPFn 的 1 数量 是 群体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2411-2411 | 中止 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2412-2412 | 中止 的 2 数量 是 过程 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2477-2477 | 中止发射 的 2 数量 是 起飞 的 instance |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2431-2431 | 任务中止 的 2 数量 是 军事行动 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4748-4748 | 绝对值函数 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1274-1274 | AccelerationFn 的 1 数量 是 函数量 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1275-1275 | AccelerationFn 的 2 数量 是 持续时间 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1276-1276 | AccelerationFn 的 3 数量 是 客体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1277-1277 | AccelerationFn 的 4 数量 是 方向属性 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2330-2330 | 帐户 的 1 数量 是 金融资产 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4698-4698 | 加法函数 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4699-4699 | 加法函数 的 2 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 223-223 | 地址 的 1 数量 是 电脑文件 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8820-8820 | AfternoonFn 的 1 数量 是 日 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 2985-2985 | 协议组织 的 1 数量 是 协议 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 929-929 | AlbumCopiesFn 的 1 数量 是 Album 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7564-7564 | AmountsFn 的 2 数量 是 躯体性物体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7565-7565 | AmountsFn 的 3 数量 是 UnitOfMass 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5245-5245 | ArcCosineFn 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5255-5255 | ArcSineFn 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5235-5235 | ArcTangentFn 的 1 数量 是 实数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 786-786 | 分派函数 的 1 数量 是 函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 787-787 | 分派函数 的 2 数量 是 实体 的 instance |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
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