2023/11/29 by Lucas Böltz, Böltz, Lucas, Viorica Sofronie-Stokkermans +3
Computer Science · #Constraint Satisfaction and Optimization #Data Management and Algorithms #FOS: Computer and information sciences #Graph Theory and Algorithms #Information Theory (cs.IT) #Logic in Computer Science (cs.LO) #Networking and Internet Architecture (cs.NI)
paper · pdf · doi:10.48550/arxiv.2311.17860
openalex publication_date 2023/11/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.