ArTS Archivio della ricerca di Trieste
ArTS è il sistema di gestione integrata dei dati della ricerca adottato dall' Università degli Studi di Trieste
EnglishAn undirected graph is commonly represented as a set of vertices and a set of vertex doubletons; but one can also represent each vertex by a finite set so as to ensure that membership mimics, over these vertex-representing sets, the edge relation of the graph. This alternative modelling, applied to connected claw-free graphs, recently gave crucial clues for obtaining simpler proofs of some of their properties (e.g. Hamiltonicity of the square of the graph). This article adds a computer-checked contribution. On the one hand, we discuss our development, by means of the Ref verifier, of two theorems on representing graphs by families of finite sets: a weaker theorem pertains to general graphs, and a stronger one to connected claw-free graphs. Before proving those theorems, we must show that every graph admits an acyclic, weakly extensional orientation, which becomes fully extensional when connectivity and claw-freeness are met. This preliminary work enables injective decoration, à la Mostowski, of the vertices by the sought-for finite sets. By this new scenario, we complement our earlier formalization with Ref of two classical properties of connected claw-free graphs. On the other hand, our present work provides another example of the ease with which graph-theoretic results are proved with the Ref verifier. For example, we managed to define and exploit the notion of connected graph without resorting to the notion of path.
| Titolo: | Set Graphs. V. On representing graphs as membership digraphs |
| Autori: | |
| Data di pubblicazione: | 2015 |
| Data ahead of print: | 13-ott-2014 |
| Stato di pubblicazione: | Pubblicato |
| Rivista: | |
| Abstract: | An undirected graph is commonly represented as a set of vertices and a set of vertex doubletons; but one can also represent each vertex by a finite set so as to ensure that membership mimics, over these vertex-representing sets, the edge relation of the graph. This alternative modelling, applied to connected claw-free graphs, recently gave crucial clues for obtaining simpler proofs of some of their properties (e.g. Hamiltonicity of the square of the graph). This article adds a computer-checked contribution. On the one hand, we discuss our development, by means of the Ref verifier, of two theorems on representing graphs by families of finite sets: a weaker theorem pertains to general graphs, and a stronger one to connected claw-free graphs. Before proving those theorems, we must show that every graph admits an acyclic, weakly extensional orientation, which becomes fully extensional when connectivity and claw-freeness are met. This preliminary work enables injective decoration, à la Mostowski, of the vertices by the sought-for finite sets. By this new scenario, we complement our earlier formalization with Ref of two classical properties of connected claw-free graphs. On the other hand, our present work provides another example of the ease with which graph-theoretic results are proved with the Ref verifier. For example, we managed to define and exploit the notion of connected graph without resorting to the notion of path. |
| Handle: | http://hdl.handle.net/11368/2840701 |
| Digital Object Identifier (DOI): | 10.1093/logcom/exu060 |
| URL: | http://logcom.oxfordjournals.org/content/early/2014/10/12/logcom.exu060.abstract https://academic.oup.com/logcom/article/25/3/899/1008487/Set-Graphs-V-On-representing-graphs-as-membership |
| Appare nelle tipologie: | 1.1 Articolo in Rivista |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| exu060.pdf | Publisher-Version | Digital Rights Management non definito | Administrator Richiedi una copia |
http://hdl.handle.net/11368/2840701
