In graph theory connectivity is stated, prevailingly, in terms of paths. While exploiting a proof assistant to check formal reasoning about graphs, we chose to work with an alternative characterization of connectivity: for, within the framework of the underlying set theory, it requires virtually no preparatory notions. We say that a graphs devoid of isolated vertices is connected if no subset of its set of edges, other than the empty set and the set of all edges, is vertex disjoint from its complementary set. Before we can work with this notion smoothly, we must prove that every connected graph has a non-cut vertex, i.e., a vertex whose removal does not disrupt connectivity. This paper presents such a proof in accurate formal terms and copes with hypergraphs to achieve greater generality.
Reasoning about connectivity without paths
CASAGRANDE, ALBERTO;OMODEO, EUGENIO
2014-01-01
Abstract
In graph theory connectivity is stated, prevailingly, in terms of paths. While exploiting a proof assistant to check formal reasoning about graphs, we chose to work with an alternative characterization of connectivity: for, within the framework of the underlying set theory, it requires virtually no preparatory notions. We say that a graphs devoid of isolated vertices is connected if no subset of its set of edges, other than the empty set and the set of all edges, is vertex disjoint from its complementary set. Before we can work with this notion smoothly, we must prove that every connected graph has a non-cut vertex, i.e., a vertex whose removal does not disrupt connectivity. This paper presents such a proof in accurate formal terms and copes with hypergraphs to achieve greater generality.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
