On the Verification of a Subgraph Construction Algorithm
summary
Automatic formalization shows the CP algorithm produces an intersection‑free connected subgraph whenever the input satisfies redundancy and coexistence by encoding Euclidean geometry, graph predicates and linked‑list paths and mechanically proving three lemmas that force a connecting path. The model uses a fragment of Hilbert axioms with 41 axioms, reduces reasoning to the decidable Bernays‑Schönfinkel class, and runs the proof obligations with an automated prover on instances up to 10 vertices, reporting fast solves but growing time with more constants.
AI-written summary · about
chapters (10)
- 0:00Subgraph verification intro
- 1:07Connected planarization algorithm
- 3:57Redundancy and coexistence
- 5:42Modeling graph properties
- 7:27Correctness proof overview
- 9:57First lemma: intersecting edges
- 11:26Edge sequences connecting components
- 12:52Convex hull path reasoning
- 13:35Conclusion and future work
- 14:37Q&A
related talks
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
01h 05mCertifying Combinatorial Solving Using Cutting Planes with Strengthening Rules
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 04mFrontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems
58mA New Perspective on Commutativity in Verification
33mConnections Between QBF Proof Complexity and Circuit Complexity
55mLower Bounds for Subgraph Isomorphism and Consequences in First-Order Logic
49mPerfection and Beyond