Über diesen Artikel
Online veröffentlicht: 17. Feb. 2020
Seitenbereich: 237 - 259
Akzeptiert: 29. Aug. 2019
DOI: https://doi.org/10.2478/forma-2019-0023
Schlüsselwörter
© 2019 Sebastian Koch, published by Sciendo
This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.
In this article the notion of the underlying simple graph of a graph (as defined in [8]) is formalized in the Mizar system [5], along with some convenient variants. The property of a graph to be without decorators (as introduced in [7]) is formalized as well to serve as the base of graph enumerations in the future.