We automatically verify the crucial steps in the original proof of correctness of an algorithm which, given a geometric graph satisfying certain additional properties removes edges in a systematic way for producing a connected graph in which edges do not (geometrically) intersect. The challenge in this case is representing and reasoning about geometric properties of graphs in the Euclidean plane, about their vertices and edges, and about connectivity. For modelling the geometric aspects, we use an axiomatization of plane geometry; for representing the graph structure we use additional predicates; for representing certain classes of paths in geometric graphs we use linked lists.

翻译：我们自动验证了一个算法正确性原始证明中的关键步骤。该算法针对满足特定附加性质的几何图，通过系统性地移除边来生成一个边之间（几何上）不相交的连通图。此案例中的挑战在于：表示并推理欧几里得平面中图的几何性质、其顶点与边的性质以及连通性。为建模几何方面，我们采用平面几何的公理化体系；为表示图结构，我们使用额外的谓词；为表示几何图中特定路径类，我们使用链表。