No TPTP formula. May not be expressible in strict first order. |
Languages.kif 3527-3527 |
基于大西洋英语的洋泾语言 是 基于英语的拼音语言 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 3545-3545 |
基于太平洋英语的洋泾浜语 是 基于英语的拼音语言 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 22144-22144 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 22143-22143 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 22142-22142 |
|