Published January 20, 2020
| Version v1
Conference paper
Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Creators
Contributors
Others:
- Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
- Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
- Preuves et Langages (PLUME) ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
- Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
- COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)
- Plume
- STAMP
- ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010)
- ANR-15-IDEX-0001,UCA JEDI,Idex UCA JEDI(2015)
- European Project: 678157,H2020,ERC-2015-STG,CoVeCe(2016)
Description
The labeled multigraphs of treewidth at most two can be described using a simple term language over which isomor-phism of the denoted graphs can be finitely axiomatized. We formally verify soundness and completeness of such an axiomatization using Coq and the mathematical components library. The completeness proof is based on a normalizing and confluent rewrite system on term-labeled graphs. While for most of the development a dependently typed representation of graphs based on finite types of vertices and edges is most convenient, we switch to a graph representation employing a fixed type of vertices shared among all graphs for establishing confluence of the rewrite system. The completeness result is then obtained by transferring confluence from the fixed-type setting to the dependently typed setting.
Abstract
International audienceAdditional details
Identifiers
- URL
- https://hal.archives-ouvertes.fr/hal-02333553
- URN
- urn:oai:HAL:hal-02333553v3
Origin repository
- Origin repository
- UNICA