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.

Set Graphs. V. On representing graphs as membership digraphs

OMODEO, EUGENIO;
2015

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.
13-ott-2014
Pubblicato
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
File in questo prodotto:
File Dimensione Formato  
exu060.pdf

non disponibili

Tipologia: Documento in Versione Editoriale
Licenza: Digital Rights Management non definito
Dimensione 2.89 MB
Formato Adobe PDF
2.89 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11368/2840701
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact