<abstract xmlns="http://www.w3.org/1999/xhtml"><p>A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system [2], based on the formalization of graphs in [6] and relations in [11], [12]. Notably, a new definition of createGraph will be given, taking only a non empty set <italic>V</italic> and a binary relation <italic>E</italic> ⊆ <italic>V × V</italic> to create a (di)graph without parallel edges, which will provide to be very useful in future articles.</p></abstract>

A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system [2], based on the formalization of graphs in [6] and relations in [11], [12]. Notably, a new definition of createGraph will be given, taking only a non empty set V and a binary relation E ⊆ V × V to create a (di)graph without parallel edges, which will provide to be very useful in future articles.

Unification of Graphs and Relations in Mizar

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Unification of Graphs and Relations in Mizar"}

A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed...

Unification of Graphs and Relations in Mizar

Online veröffentlicht: 09. Jan. 2021

Seitenbereich: 173 - 186

Akzeptiert: 31. Mai 2020

DOI: https://doi.org/10.2478/forma-2020-0015

Schlüsselwörter
graph theory, binary relation

© 2020 Sebastian Koch, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Unification of Graphs and Relations in Mizar

Online veröffentlicht: 09. Jan. 2021

Seitenbereich: 173 - 186

Akzeptiert: 31. Mai 2020

DOI: https://doi.org/10.2478/forma-2020-0015

Schlüsselwörtergraph theory, binary relation

© 2020 Sebastian Koch, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Schlüsselwörter
graph theory, binary relation