No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1536-1536 |
英语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14973-14973 |
法语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14978-14978 |
德国的语言 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14983-14983 |
希腊语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14987-14987 |
拉丁语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14992-14992 |
俄语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14996-14996 |
西班牙语 是 自然语言 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1447-1447 |
人类语言 详尽无遗地 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 55-55 |
|
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 |
|