| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3725-3726 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16640-16643 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16638-16638 | 雇用 的 1 数量 是 施事体 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16639-16639 | 雇用 的 2 数量 是 有认知的主事 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16637-16637 | 雇用 是 二元谓语 的 instance |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 547-547 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 552-552 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 321-321 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 91-91 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2089-2089 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 273-273 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 327-327 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 715-715 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 131-131 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 342-342 | |
| No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 355-355 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 197-197 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22002-22002 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 548-548 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22001-22001 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22000-22000 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 198-198 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3260-3266 | 协议 employs 另一个 协议 若且唯若 有存在 有认知的主事 这样 那个 有认知的主事 有 雇用 的 attribute 和 那个 协议 是 那个 有认知的主事 的 party 协议 和 那个 另外 协议 是 那个 有认知的主事 的 party 协议 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17254-17262 | 实体 是 人类 的 instance 和 对所有 另一个 实体 那个 另外 实体 doesn't employs 那个 实体 在 时间位置 holdsDuring 若且唯若 失业的 是 那个 实体 的 attribute 在 那个 时间位置 holdsDuring |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2215-2219 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20601-20623 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2392-2407 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1522-1535 |
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3040-3054 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3022-3038 |
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1180-1185 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1192-1207 |
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3590-3601 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17282-17285 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3635-3642 | 有认知的主事 对于 %3 的 customer 代表 若且唯若 有存在 过程 这样 那个 过程 是 金融交易 的 instance 和 机构 employs 那个 有认知的主事 和 那个 有认知的主事 是 那个 过程 的 agent 和 那个 过程 在 另一个 有认知的主事 结束 |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1935-1946 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 4486-4490 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 4492-4496 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 171-177 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10740-10748 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10724-10732 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 10620-10629 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16916-16923 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1902-1914 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 4614-4619 | |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 4607-4612 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20998-21004 | |
| No TPTP formula. May not be expressible in strict first order. | naics.kif 11934-11946 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1883-1888 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16838-16844 | |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3357-3364 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22414-22419 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22965-22974 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3122-3129 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3084-3092 | |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2281-2292 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8544-8557 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22560-22574 |
|
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2300-2307 |
|
| 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. | Medicine.kif 4590-4593 | 有存在 有认知的主事 这样 NewReporter 是 那个 有认知的主事 的 attribute 和 ProPublica employs 那个 有认知的主事 |
|
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