![]() |
![]() ![]() ![]()
|
![]() |
|
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2400-2401 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6122-6125 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6120-6120 | NonCompositeUnitOfMeasure is a subclass of constant quantity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6119-6119 | NonCompositeUnitOfMeasure is a subclass of unit of measure |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2544-2544 | PH value is an instance of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6222-6222 | UnitOfAngularMeasure is a subclass of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6212-6212 | UnitOfCurrency is a subclass of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6243-6243 | UnitOfDuration is a subclass of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6237-6237 | UnitOfInformation is a subclass of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6151-6151 | UnitOfLength is a subclass of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6163-6163 | UnitOfMass is a subclass of NonCompositeUnitOfMeasure |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6199-6199 | UnitOfTemperature is a subclass of NonCompositeUnitOfMeasure |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6127-6127 | Unit of measure is exhaustively partitioned into CompositeUnitOfMeasure and NonCompositeUnitOfMeasure |
antecedent |
![]() |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6365-6369 |
|
![]() |
![]() |