Abstract
The previous articles [5] and [6] introduced formalizations of the step-by-step operations we use to construct finite graphs by hand. That implicitly showed that any finite graph can be constructed from the trivial edgeless graph K1 by applying a finite sequence of these basic operations. In this article that claim is proven explicitly with Mizar[4].
Language: English
Page range: 153 - 179
Accepted on: May 27, 2019
Published on: Jul 20, 2019
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Related subjects:
© 2019 Sebastian Koch, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.