| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Graph Theory
| Title: | Graph Theory |
| Author: | Lars Noschinski |
| Submission date: | 2013-04-28 |
| Abstract: | This development provides a formalization of directed graphs, supporting (labelled) multi-edges and infinite graphs. A polymorphic edge type allows edges to be treated as pairs of vertices, if multi-edges are not required. Formalized properties are i.a. walks (and related concepts), connectedness and subgraphs and basic properties of isomorphisms.
This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs. |
| BibTeX: |
@article{Graph_Theory-AFP,
author = {Lars Noschinski},
title = {Graph Theory},
journal = {Archive of Formal Proofs},
month = apr,
year = 2013,
note = {\url{http://isa-afp.org/entries/Graph_Theory.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Parity_Game, Planarity_Certificates, ShortestPath |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |