| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1683-1683 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1545-1546 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1543-1543 | 施事体 是 客体 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3686-3686 | 家具 和 % 2 是 disjoint |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6683-6683 | 街道地址 的 range 是 施事体 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16066-16066 | 商业代理人 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13947-13947 | 地缘政治区域 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16117-16117 | 群组 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 1305-1305 | IT代理商 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14248-14248 | 生物 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16503-16503 | 机构 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1553-1553 | 有感知的主事 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 848-848 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 64508-64508 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 898-898 |
| appearance as argument number 3 |
|
|
| 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. | Government.kif 1685-1685 | 选举 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1321-1321 | 行政部门 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3713-3713 | 财政年度 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3739-3739 | 财政年度开始 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4261-4261 | 属于财产函数 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1178-1178 | SellersItemsFn 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1213-1213 | SellersOtherItemsFn 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7778-7778 | 财富函数 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1660-1660 | 成就 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 596-596 | activityCapability 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2421-2421 | 主事 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3423-3423 | agentName 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2235-2235 | 代理人在区域内经营 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23159-23159 | 别号 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Biography.kif 150-150 | appointedPosition 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22879-22879 | 所负责的地区 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23430-23430 | 逮捕 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1942-1942 | 问价格 的 3 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2424-2424 | 在组织中关联 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2435-2435 | 与地位相关联 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | emotion.kif 2126-2126 | attitudeForFormula 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | emotion.kif 2119-2119 | attitudeForObject 的 2 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15349-15349 | 作者 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22864-22864 | 得益 的 2 数量 是 施事体 的 instance |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1774-1779 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30143-30154 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1700-1704 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1767-1772 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1189-1205 |
|
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 772-795 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1692-1698 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1509-1521 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 437-448 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11610-11620 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1230-1257 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4563-4580 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11627-11639 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 472-479 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2501-2508 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 393-405 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1447-1453 | |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2830-2844 |
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 1478-1485 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3754-3758 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1702-1724 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3162-3189 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1776-1787 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3205-3232 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4057-4068 | |
| 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 30124-30137 | Alone 是 实体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 那个 实体2 和 过程 这样 那个 实体 不 equal 那个 实体2 和 那个 实体2 是 施事体 的 instance 和 那个 过程 是 社交 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 实体 是事件 那个 过程 的 involved 和 那个 实体2 是事件 那个 过程 的 involved |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 784-792 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3734-3738 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3782-3786 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 426-435 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23409-23413 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15822-15835 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4563-4580 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16121-16125 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3582-3614 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3681-3713 |
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 895-901 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16524-16528 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2632-2641 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2047-2064 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1933-1952 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1965-1984 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1997-2016 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2028-2045 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3829-3833 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 1026-1030 | |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 956-980 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 921-932 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 766-773 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4551-4561 | |
| 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