No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1536-1536 |
例 英語 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14972-14972 |
例 法語 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14977-14977 |
例 德國的語言 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14982-14982 |
例 希臘語 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14986-14986 |
例 拉丁語 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14991-14991 |
例 俄語 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14995-14995 |
例 西班牙語 and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1447-1447 |
劃分 HumanLanguage, NaturalLanguage and ConstructedLanguage |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 14594-14594 |
子類 ChineseLanguage and NaturalLanguage |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 12647-12647 |
子類 LanguageFamily and NaturalLanguage |
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 |
|