Spanning Tree

The aim is to prove that every connected graph has a spanning tree (slides).

Specification

See tree.maude for the full specification.

Verification

In the attempt of proving that every connected graph has a spanning tree, we realized that it is much easier to prove that every graph has a spanning forest.

A spanning forest of a graph is a subgraph that consists of a set of spanning trees, one for each maximally connected component of the initial graph.

mktree preserves the maximal connected componets of each vertex.

GRAPH |- mcc(A, mktree(G)) = mcc(A, G) ;

See th1.maude for the full proof.

mktree preserves the number of maximally connected componets.

GRAPH |- nomcc(mktree(G)) = nomcc(G) ;

See th2.maude for the full proof.

mktree eliminates the cycles.

GRAPH |- nocycle(mktree(G)) = true ;

See th3.maude for the full proof.