(=>
(and
(totalLengthOfHighwaySystem ?AREA
(MeasureFn ?LENGTH ?UNIT))
(lengthOfPavedHighway ?AREA
(MeasureFn ?LENGTH1 ?UNIT))
(lengthOfUnpavedHighway ?AREA
(MeasureFn ?LENGTH2 ?UNIT)))
(equal ?LENGTH
(AdditionFn ?LENGTH1 ?LENGTH2))) |
Transportation.kif 503-508 |
If X Y(s) is a total length of highway system of Z, W Y(s) is a length of paved highway of Z, and V Y(s) is a length of unpaved highway of Z, then equal X and (W and V) |
(=>
(and
(totalLengthOfHighwaySystem ?AREA
(MeasureFn ?LENGTH ?UNIT))
(lengthOfPavedHighway ?AREA
(MeasureFn ?LENGTH1 ?UNIT))
(lengthOfUnpavedHighway ?AREA
(MeasureFn ?LENGTH2 ?UNIT))
(instance ?UNIT UnitOfLength))
(totalLengthOfHighwaySystem ?AREA
(MeasureFn
(AdditionFn ?LENGTH1 ?LENGTH2) ?UNIT))) |
Transportation.kif 510-517 |
If X Y(s) is a total length of highway system of Z, W Y(s) is a length of paved highway of Z, V Y(s) is a length of unpaved highway of Z, and Y is an instance of unit of length, then (W and V) Y(s) is a total length of highway system of Z |
(=>
(and
(totalLengthOfHighwaySystem ?AREA
(MeasureFn ?TOTAL ?UNIT))
(lengthOfPavedHighway ?AREA
(MeasureFn ?PAVED ?UNIT)))
(greaterThanOrEqualTo ?TOTAL ?PAVED)) |
Transportation.kif 519-525 |
If X Y(s) is a total length of highway system of Z and W Y(s) is a length of paved highway of Z, then X is greater than or equal to W |
(<=>
(lengthOfPavedHighway ?AREA ?LENGTH)
(length
(KappaFn ?HIGHWAYS
(and
(instance ?HIGHWAYS SurfacedRoadway)
(located ?HIGHWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 542-549 |
X is a length of paved highway of Y if and only if the length of the class described by Z is X |
(=>
(and
(lengthOfPavedHighway ?AREA
(MeasureFn ?LENGTH ?UNIT))
(instance ?UNIT UnitOfLength)
(greaterThan ?LENGTH 0))
(exists (?HIGHWAY)
(and
(instance ?HIGHWAY SurfacedRoadway)
(located ?HIGHWAY ?AREA)))) |
Transportation.kif 551-559 |
If X Y(s) is a length of paved highway of Z, Y is an instance of unit of length, and X is greater than 0, then there exists W such that W is an instance of surfaced roadway and W is located at Z |
(=>
(and
(instance ?UNIT UnitOfLength)
(lengthOfExpresswaySystem ?AREA
(MeasureFn ?LENGTH1 ?UNIT))
(lengthOfPavedHighway ?AREA
(MeasureFn ?LENGTH2 ?UNIT)))
(greaterThanOrEqualTo ?LENGTH2 ?LENGTH1)) |
Transportation.kif 587-592 |
If X is an instance of unit of length, Y X(s) is a length of expressway system of Z, and W X(s) is a length of paved highway of Z, then W is greater than or equal to Y |
