No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1536-1536 |
English language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14973-14973 |
French language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14978-14978 |
German language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14983-14983 |
Greek language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14987-14987 |
Latin language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14992-14992 |
Russian language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14996-14996 |
Spanish language is an instance of natural language |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1447-1447 |
Human language is exhaustively partitioned into natural language and constructed language |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 14594-14594 |
Chinese language is a subclass of natural language |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 12647-12647 |
Language family is a subclass of natural language |
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 |
|