( ! [V__GRAPH] :
((s__instance(V__GRAPH,s__MultiGraph) =>
( ? [V__ARC1, V__ARC2, V__NODE1, V__NODE2] :
((s__instance(V__ARC1,s__GraphArc) &
s__instance(V__ARC2,s__GraphArc) &
s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
(s__graphPart(V__ARC1,V__GRAPH)
&
s__graphPart(V__ARC2,V__GRAPH)
&
s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
s__links(V__NODE1,V__NODE2,V__ARC1)
&
s__links(V__NODE1,V__NODE2,V__ARC2)
&
~((V__ARC1 = V__ARC2)))))))
&
(( ? [V__ARC1, V__ARC2, V__NODE1, V__NODE2] :
((s__instance(V__ARC1,s__GraphArc) &
s__instance(V__ARC2,s__GraphArc) &
s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
(s__graphPart(V__ARC1,V__GRAPH)
&
s__graphPart(V__ARC2,V__GRAPH)
&
s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
s__links(V__NODE1,V__NODE2,V__ARC1)
&
s__links(V__NODE1,V__NODE2,V__ARC2)
&
~((V__ARC1 = V__ARC2))))))
=>
s__instance(V__GRAPH,s__MultiGraph))
)
)
|
Merge.kif 5442-5452 |
A graph is an instance of multi graph if and only if there exist a graph arc, another graph arc,, , a graph node and another graph node such that the graph arc is a part of the graph and the other graph arc is a part of the graph and the graph node is a part of the graph and the other graph node is a part of the graph and the graph arc links the graph node and the other graph node and the other graph arc links the graph node and the other graph node and the graph arc is not equal to the other graph arc |
( ! [V__LOOP] :
((s__instance(V__LOOP,s__GraphLoop) =>
( ? [V__NODE] :
((s__instance(V__NODE,s__GraphNode) &
s__links(V__NODE,V__NODE,V__LOOP)))))
&
(( ? [V__NODE] :
((s__instance(V__NODE,s__GraphNode) &
s__links(V__NODE,V__NODE,V__LOOP))))
=>
s__instance(V__LOOP,s__GraphLoop))
)
)
|
Merge.kif 5504-5507 |
A graph arc is an instance of graph loop if and only if there exists a graph node such that the graph arc links the graph node and the graph node |
( ! [V__NODE2,V__NODE1,V__A,V__N1,V__N2,V__ARC] :
((s__instance(V__NODE2,s__Object) &
s__instance(V__NODE1,s__Object) &
s__instance(V__A,s__Object) &
s__instance(V__N1,s__GraphNode) &
s__instance(V__N2,s__GraphNode) &
s__instance(V__ARC,s__GraphArc))
=>
(s__connects(V__A,V__NODE1,V__NODE2)
&
s__abstractCounterpart(V__N1,V__NODE1)
&
s__abstractCounterpart(V__N2,V__NODE2)
&
s__abstractCounterpart(V__ARC,V__A))
=>
s__links(V__N1,V__N2,V__ARC)
)
)
|
Transportation.kif 2848-2854 |
|
( ! [V__NODE2,V__NODE1,V__GRAPH] :
((s__instance(V__GRAPH,s__Graph) &
s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
~((V__NODE1 = V__NODE2)))
=>
( ? [V__ARC, V__PATH] :
((s__instance(V__ARC,s__GraphArc) &
(s__links(V__NODE1,V__NODE2,V__ARC)
|
(s__subGraph(V__PATH,V__GRAPH)
&
s__instance(V__PATH,s__GraphPath) &
(((s__BeginNodeFn(V__PATH)
= V__NODE1)
&
(s__EndNodeFn(V__PATH)
= V__NODE2))
|
((s__BeginNodeFn(V__PATH)
= V__NODE2)
&
(s__EndNodeFn(V__PATH)
= V__NODE1))))))))
)
)
|
Merge.kif 5303-5323 |
|
( ! [V__ARC] :
(s__instance(V__ARC,s__GraphArc) =>
( ? [V__NODE1, V__NODE2] :
((s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__links(V__NODE1,V__NODE2,V__ARC))))
)
)
|
Merge.kif 5494-5497 |
|
( ! [V__GRAPH] :
(s__instance(V__GRAPH,s__Graph) =>
( ? [V__NODE1, V__NODE2, V__NODE3, V__ARC1, V__ARC2] :
((s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__instance(V__NODE3,s__GraphNode) &
s__instance(V__ARC1,s__GraphArc) &
s__instance(V__ARC2,s__GraphArc) &
(s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
s__graphPart(V__NODE3,V__GRAPH)
&
s__graphPart(V__ARC1,V__GRAPH)
&
s__graphPart(V__ARC2,V__GRAPH)
&
s__links(V__NODE1,V__NODE2,V__ARC1)
&
s__links(V__NODE2,V__NODE3,V__ARC2)
&
~((V__NODE1 = V__NODE2))
&
~((V__NODE2 = V__NODE3))
&
~((V__NODE1 = V__NODE3))
&
~((V__ARC1 = V__ARC2))))))
)
)
|
Merge.kif 5325-5339 |
|
( ! [V__NODE] :
(s__instance(V__NODE,s__GraphNode) =>
( ? [V__OTHER, V__ARC] :
((s__instance(V__OTHER,s__GraphNode) &
s__instance(V__ARC,s__GraphArc) &
s__links(V__NODE,V__OTHER,V__ARC))))
)
)
|
Merge.kif 5484-5487 |
|
( ! [V__NODE2,V__NODE1,V__ARC] :
((s__instance(V__NODE2,s__GraphNode) &
s__instance(V__NODE1,s__GraphNode) &
s__instance(V__ARC,s__GraphArc))
=>
s__links(V__NODE1,V__NODE2,V__ARC)
=>
s__links(V__NODE2,V__NODE1,V__ARC)
)
)
|
Merge.kif 5523-5525 |
|
