No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1523-1523 |
英语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14843-14843 |
法语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14848-14848 |
德国的语言 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14853-14853 |
希腊语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14857-14857 |
拉丁语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14862-14862 |
俄语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14866-14866 |
西班牙语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1434-1434 |
人类语言 详尽无遗地 partition 成 自然语言 和 人工语言 |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 14594-14594 |
ChineseLanguage 是 自然语言 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 12647-12647 |
LanguageFamily 是 自然语言 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 845-845 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 892-892 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 521-521 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 52-52 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 53-53 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2206-2206 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 473-473 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 57-57 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 88-88 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 542-542 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 56-56 |
|