Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| UnitFn |
| appearance as argument number 1 |
|
| (instance UnitFn UnaryFunction) | Merge.kif 6728-6728 | Unit fn is an instance of unary function |
| (instance UnitFn TotalValuedRelation) | Merge.kif 6729-6729 | Unit fn is an instance of total valued relation |
| (domain UnitFn 1 PhysicalQuantity) | Merge.kif 6730-6730 | The number 1 argument of unit fn is an instance of physical quantity |
| (range UnitFn UnitOfMeasure) | Merge.kif 6731-6731 | The range of unit fn is an instance of unit of measure |
| (documentation UnitFn EnglishLanguage "UnitFn returns just the UnitOfMeasure of a PhysicalQuantity with an associated UnitOfMeasure and RealNumber magnitude. For example, the unit of the ConstantQuantity (MeasureFn 2 Kilometer) is the UnitOfMeasure Kilometer.") | Merge.kif 6733-6737 | The range of unit fn is an instance of unit of measure |
| appearance as argument number 2 |
|
|
| (format EnglishLanguage UnitFn "the unit of %1") | domainEnglishFormat.kif 4874-4874 | |
| (format ChineseTraditionalLanguage UnitFn "%1 的 unit ") | domainEnglishFormat.kif 4875-4875 | |
| (format ChineseLanguage UnitFn "%1 的 unit ") | domainEnglishFormat.kif 4876-4876 | |
| (termFormat EnglishLanguage UnitFn "unit fn") | domainEnglishFormat.kif 65653-65653 |
| consequent |
|
|
| (=> (and (instance ?QUANT PhysicalQuantity) (instance ?UNIT UnitOfMeasure) (equal ?QUANT (MeasureFn ?NUMBER ?UNIT))) (equal (UnitFn ?QUANT) ?UNIT)) |
Merge.kif 6739-6745 | If X is an instance of physical quantity, Y is an instance of unit of measure, and equal X and Z Y(s), then equal the unit of X and Y |
|