(=>
(instance ?SYSTEM TransitSystem)
(exists (?ROUTE)
(and
(instance ?ROUTE Transitway)
(part ?ROUTE ?SYSTEM)))) |
Transportation.kif 3973-3978 |
If X is an instance of transit system, then there exists Y such that Y is an instance of transitway and Y is a part of X |
(=>
(instance ?TS TransitSystem)
(exists (?G)
(and
(instance ?G Graph)
(abstractCounterpart ?G ?TS)))) |
Transportation.kif 3980-3985 |
If X is an instance of transit system, then there exists Y such that Y is an instance of graph and the abstract counterpart of X is Y |
(=>
(and
(instance ?TS TransitSystem)
(instance ?T Transitway)
(abstractCounterpart ?G ?TS)
(systemPart ?T ?TS))
(exists (?GA)
(and
(instance ?GA GraphArc)
(abstractCounterpart ?GA ?T)
(graphPart ?GA ?G)))) |
Transportation.kif 3987-3997 |
If X is an instance of transit system, Y is an instance of transitway, the abstract counterpart of X is Z, and X is a system part of Y, then there exists W such that W is an instance of graph arc, the abstract counterpart of Y is W, and W is a part of Z |
(=>
(and
(instance ?TS TransitSystem)
(instance ?TJ TransitwayJunction)
(abstractCounterpart ?G ?TS)
(systemPart ?TJ ?TS))
(exists (?GN)
(and
(instance ?GN GraphNode)
(abstractCounterpart ?GN ?TJ)
(graphPart ?GN ?G)))) |
Transportation.kif 3999-4009 |
If X is an instance of transit system, Y is an instance of transitway junction, the abstract counterpart of X is Z, and X is a system part of Y, then there exists W such that W is an instance of graph node, the abstract counterpart of Y is W, and W is a part of Z |
(=>
(and
(instance ?SYSTEM TransitSystem)
(systemPart ?PART ?SYSTEM))
(instance ?PART Transitway)) |
Transportation.kif 4019-4023 |
If X is an instance of transit system and X is a system part of Y, then Y is an instance of transitway |
