| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1490-1491 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 308-310 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 50-52 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 55-57 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 306-306 | 范围 的 1 数量 是 函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 307-307 | 范围 的 2 数量 是 类 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 305-305 | 范围 是 非对称关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 304-304 | 范围 是 二元谓语 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 313-313 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 318-318 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 179-179 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 238-238 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1999-1999 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 131-131 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 180-180 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 410-410 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 276-276 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 199-199 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 189-189 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 430-430 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 314-314 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48757-48757 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 48756-48756 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3392-3396 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 312-316 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 324-330 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 433-438 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 318-322 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 318-322 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3227-3227 | ABPFn 的 range 是 货币测量 的实例 |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3272-3272 | ASPFn 的 range 是 货币测量 的实例 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2413-2413 | 中止 的 range 是 过程 的实例 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2478-2478 | 中止发射 的 range 是 起飞 的实例 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2432-2432 | 任务中止 的 range 是 军事行动 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4763-4763 | 绝对值函数 的 range 是 非负实数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1280-1280 | AccelerationFn 的 range 是 函数量 的实例 |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2317-2317 | 帐户 的 range 是 金融账户 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4714-4714 | 加法函数 的 range 是 实数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 224-224 | 地址 的 range 是 实际地址 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8835-8835 | AfternoonFn 的 range 是 下午 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3057-3057 | 协议组织 的 range 是 机构 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7580-7580 | AmountsFn 的 range 是 串列 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5260-5260 | ArcCosineFn 的 range 是 实数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5270-5270 | ArcSineFn 的 range 是 实数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5250-5250 | ArcTangentFn 的 range 是 实数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 788-788 | 分派函数 的 range 是 实体 的实例 |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3195-3195 | AuctionGMBFn 的 range 是 货币测量 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 866-866 | 可用于兵役男性 的 range 是 整数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3272-3272 | AverageFn 的 range 是 实数 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 899-899 | 挪后函数 的 range 是 自身连接物体 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7983-7983 | 开始函数 的 range 是 时点 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5943-5943 | 节点开端函数 的 range 是 图节点 的实例 |
| No TPTP formula. May not be expressible in strict first order. | People.kif 674-674 | BeliefGroupMemberFn 的 range 是 内在属性 的实例 |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2914-2914 | BidCountFn 的 range 是 非负整数 的实例 |
| 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