Version 1 (modified by onnopaap, 14 years ago) |
---|
Base Template LowerUpperMagnitudeOfPropertyRange
LowerUpperMagnitudeOfPropertyRange is a template for expressing the extent of a property range, in terms of maximum and minimum values on a scale.
LowerUpperMagnitudeOfPropertyRange(a, b, c, d) means that a is a property range, b is a scale, and c and d are numbers, and that a has c and d as, respectively, lower and upper bounds, as measured on the scale b.
Roles:
1 hasPropertyRange PropertyRange
2 hasScale Scale
3 hasLowerBound ArithmeticNumber
4 hasUpperBound ArithmeticNumber
Axiom:
LowerUpperMagnitudeOfPropertyRange(x1, x2, x3, x4) <-> PropertyRange(x1) & Scale(x2) & ArithmeticNumber(x3) & ArithmeticNumber(x4) & exists y1, y2(LowerUpperOfPropertyRange(x1, y1, y2) & MagnitudeOfProperty(y1, x3, x2) & MagnitudeOfProperty(y2, x4, x2)) .