No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2143-2147 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4342-4347 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 799-803 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4338-4338 |
域子類 preventsSubclass, 1 and Process |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4339-4339 |
域子類 preventsSubclass, 2 and Process |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4335-4335 |
例 preventsSubclass and BinaryPredicate |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4336-4336 |
例 preventsSubclass and IrreflexiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4337-4337 |
例 preventsSubclass and PartialValuedRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4340-4340 |
相關的內部概念 preventsSubclass and hindersSubclass |