(=>
(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))
(lengthOfUnpavedHighway ?AREA
(MeasureFn ?UNPAVED ?UNIT)))
(greaterThanOrEqualTo ?TOTAL ?UNPAVED)) |
Transportation.kif 527-533 |
If X Y(s) is a total length of highway system of Z and W Y(s) is a length of unpaved highway of Z, then X is greater than or equal to W |
(<=>
(lengthOfUnpavedHighway ?AREA ?LENGTH)
(length
(KappaFn ?HIGHWAYS
(and
(instance ?HIGHWAYS UnsurfacedRoadway)
(located ?HIGHWAYS ?AREA))) ?LENGTH)) |
Transportation.kif 601-608 |
X is a length of unpaved highway of Y if and only if the length of the class described by Z is X |
(=>
(and
(lengthOfUnpavedHighway ?AREA
(MeasureFn ?LENGTH ?UNIT))
(instance ?UNIT UnitOfLength)
(greaterThan ?LENGTH 0))
(exists (?HIGHWAY)
(and
(instance ?HIGHWAY UnsurfacedRoadway)
(located ?HIGHWAY ?AREA)))) |
Transportation.kif 610-618 |
If X Y(s) is a length of unpaved 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 unsurfaced roadway and W is located at Z |
