No TPTP formula. May not be expressible in strict first order. | Merge.kif 3398-3398 | 子類 BinaryFunction and Function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3399-3399 | 子類 BinaryFunction and TernaryRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3400-3400 | 子類 BinaryFunction and 可繼承的關係 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3409-3409 | 子類 AssociativeFunction and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3430-3430 | 子類 CommutativeFunction and BinaryFunction |