Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
summary
Formal proof in Coq (MathComp) shows completeness: an 11‑axiom equational theory proves two terms equivalent iff their interpreted directed labeled graphs are isomorphic. Key work is mechanizing a confluent graph rewrite system that gives reducibility and confluence, using two complementary graph encodings (additive representation, subtractive representation) and transfers between them. The development is ~5,000 LOC, local confluence handles ~15 symmetry-broken cases, and the mechanization succeeds with no remaining holes.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:12What is axiomatic graph isomorphism
- 1:17What are multigraphs
- 1:39Interpretation of terms as graphs
- 3:24Completeness
- 3:45Proof
- 5:47Generalization
- 7:17Rewrite System
- 8:18Representation
- 9:32Additive Representation
- 10:39Second Representation
- 12:30Proof Structure
- 13:47Conclusion
- 15:24Wrapup
related talks
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
31mA Coq Library of Undecidable Problems
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
14mAdequacy for Algebraic Effects Revisited
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
27mAn Equations Tutorial