|
|
   Character
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1645-1647 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1342-1345 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 230-233 | |
| No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 272-275 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1340-1340 | 字符 是 符号串 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19465-19465 | 字母字符 是 字符 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19469-19469 | 数字字符 是 字符 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 835-835 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 872-872 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 511-511 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 43-43 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 46-46 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2196-2196 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 463-463 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 48-48 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 78-78 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 532-532 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 47-47 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24370-24370 | inString 的 1 数量 是 字符 的 instance |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2904-2909 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2912-2917 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24377-24382 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1347-1352 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 679-688 |
|
|
|