UnitOfLength |
appearance as argument number 1 |
![]() |
(documentation UnitOfLength ChineseLanguage "这个 Class 所有的实例都是可以用 MeasureFn 来 组成 LengthMeasure 实例的 UnitOfMeasure。") | chinese_format.kif 2405-2406 | |
(documentation UnitOfLength EnglishLanguage "Every instance of this Class is a UnitOfMeasure that can be used with MeasureFn to form instances of LengthMeasure.") | Merge.kif 5813-5815 | |
(subclass UnitOfLength NonCompositeUnitOfMeasure) | Merge.kif 5811-5811 | subclass UnitOfLength and NonCompositeUnitOfMeasure |
appearance as argument number 2 |
![]() |
antecedent |
![]() |
consequent |
![]() |
(<=> (larger ?OBJ1 ?OBJ2) (forall (?QUANT1 ?QUANT2 ?UNIT) (=> (and (measure ?OBJ1 (MeasureFn ?QUANT1 ?UNIT)) (measure ?OBJ2 (MeasureFn ?QUANT2 ?UNIT)) (instance ?UNIT UnitOfLength)) (greaterThan ?QUANT1 ?QUANT2)))) |
Merge.kif 7234-7242 | larger Object and Object RealNumber RealNumber and UnitOfMeasure
|
![]() |
![]() |