No TPTP formula. May not be expressible in strict first order. |
Merge.kif 784-784 |
分派函数 是 函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4844-4844 |
最大公因数函数 是 函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 405-405 |
纬度 是 函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4929-4929 |
最小公倍数函数 是 函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2931-2931 |
表列函数 是 函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 442-442 |
经度 是 函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3398-3398 |
二元函数 是 函数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3472-3472 |
连续函数 是 函数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3461-3461 |
四元函数 是 函数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3450-3450 |
三元函数 是 函数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3358-3358 |
一元函数 是 函数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 916-916 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1039-1039 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 592-592 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 122-122 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 125-125 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2277-2277 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 544-544 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 127-127 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 159-159 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 613-613 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 126-126 |
|