(<=>
(totalFacilityTypeInArea ?AREA ?TYPE ?COUNT)
(cardinality
(KappaFn ?ITEM
(and
(instance ?ITEM ?TYPE)
(located ?ITEM ?AREA))) ?COUNT)) |
Transportation.kif 1221-1228 |
X is total facility type in area Y for Z if and only if Z is a cardinality of the class described by W |
(=>
(totalFacilityTypeInArea ?AREA ?TYPE ?COUNT)
(exists (?ITEM)
(and
(instance ?ITEM ?TYPE)
(located ?ITEM ?AREA)))) |
Transportation.kif 1230-1235 |
If X is total facility type in area Y for Z, then there exists W such that W is an instance of Y and W is located at X |
(=>
(and
(totalFacilityTypeInArea ?AREA ?TYPE ?COUNT)
(equal ?COUNT 0))
(not
(exists (?ITEM)
(and
(instance ?ITEM ?TYPE)
(located ?ITEM ?AREA))))) |
Transportation.kif 1237-1245 |
If X is total facility type in area Y for Z and equal Z and 0, then there doesn't exist W such that W is an instance of Y and W is located at X |
(<=>
(totalFacilityTypeInArea ?AREA
(ExtensionFn AirportWithPavedRunway) ?COUNT)
(exists (?AIRPORT ?RUNWAY)
(cardinality
(KappaFn ?AIRPORT
(and
(instance ?AIRPORT Airport)
(instance ?RUNWAY PavedRunway)
(part ?RUNWAY ?AIRPORT)
(located ?AIRPORT ?AREA))) ?COUNT))) |
Transportation.kif 1349-1359 |
X is total facility type in area the class corresponding to airport with paved runway for Y if, only if there exist Z, and W such that Y is a cardinality of the class described by Z |
(=>
(totalFacilityTypeInArea ?AREA
(ExtensionFn AirportWithPavedRunway) ?COUNT)
(exists (?AIRPORT ?RUNWAY)
(and
(instance ?AIRPORT Airport)
(instance ?RUNWAY PavedRunway)
(part ?RUNWAY ?AIRPORT)
(located ?AIRPORT ?AREA)))) |
Transportation.kif 1361-1368 |
If X is total facility type in area the class corresponding to airport with paved runway for Y, then there exist Z, W such that Z is an instance of airport, W is an instance of paved runway, W is a part of Z, and Z is located at X |
(=>
(and
(totalFacilityTypeInArea ?AREA
(ExtensionFn AirportWithUnpavedRunway) ?COUNT)
(greaterThan ?COUNT 0))
(exists (?AIRPORT ?RUNWAY)
(and
(instance ?AIRPORT Airport)
(instance ?RUNWAY UnpavedRunway)
(part ?RUNWAY ?AIRPORT)
(located ?AIRPORT ?AREA)))) |
Transportation.kif 1627-1636 |
If X is total facility type in area the class corresponding to airport with unpaved runway for Y and Y is greater than 0, then there exist Z, W such that Z is an instance of airport, W is an instance of unpaved runway, W is a part of Z, and Z is located at X |