<abstract xmlns="http://www.w3.org/1999/xhtml">In the previous article <xref ref-type="bibr" rid="j_forma-2018-0010_ref_005_w2aab3b7b2b1b6b1ab1ab5Aa">[5]</xref> supergraphs and several specializations to formalize the process of drawing graphs were introduced. In this paper another such operation is formalized in Mizar <xref ref-type="bibr" rid="j_forma-2018-0010_ref_001_w2aab3b7b2b1b6b1ab1ab1Aa">[1]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0010_ref_002_w2aab3b7b2b1b6b1ab1ab2Aa">[2]</xref>: drawing a vertex and then immediately drawing edges connecting this vertex with a subset of the other vertices of the graph. In case the new vertex is joined with all vertices of a given graph <italic>G</italic>, this is known as the join of <italic>G</italic> and the trivial loopless graph <italic>K</italic>1. While the join of two graphs is known and found in standard literature (like <xref ref-type="bibr" rid="j_forma-2018-0010_ref_009_w2aab3b7b2b1b6b1ab1ab9Aa">[9]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0010_ref_004_w2aab3b7b2b1b6b1ab1ab4Aa">[4]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0010_ref_008_w2aab3b7b2b1b6b1ab1ab8Aa">[8]</xref> and <xref ref-type="bibr" rid="j_forma-2018-0010_ref_003_w2aab3b7b2b1b6b1ab1ab3Aa">[3]</xref>), the operation discribed in this article is not.Alongside the new operation a mode to reverse the directions of a subset of the edges of a graph is introduced. When all edge directions of a graph are reversed, this is commonly known as the converse of a (directed) graph.</abstract>

In the previous article [5] supergraphs and several specializations to formalize the process of drawing graphs were introduced. In this paper another such operation is formalized in Mizar [1], [2]: drawing a vertex and then immediately drawing edges connecting this vertex with a subset of the other vertices of the graph. In case the new vertex is joined with all vertices of a given graph G, this is known as the join of G and the trivial loopless graph K1. While the join of two graphs is known and found in standard literature (like [9], [4], [8] and [3]), the operation discribed in this article is not.Alongside the new operation a mode to reverse the directions of a subset of the edges of a graph is introduced. When all edge directions of a graph are reversed, this is commonly known as the converse of a (directed) graph.

About Supergraphs. Part II

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"About Supergraphs. Part II"}

In the previous article [5] supergraphs and several specializations to formalize the process of drawing graphs were introduced. In this paper another such...

About Supergraphs. Part II

Online veröffentlicht: 24. Dez. 2018

Seitenbereich: 125 - 140

Akzeptiert: 29. Juni 2018

DOI: https://doi.org/10.2478/forma-2018-0010

Schlüsselwörter
supergraph, graph operations

© 2018 Sebastian Koch, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

About Supergraphs. Part II

Online veröffentlicht: 24. Dez. 2018

Seitenbereich: 125 - 140

Akzeptiert: 29. Juni 2018

DOI: https://doi.org/10.2478/forma-2018-0010

Schlüsselwörtersupergraph, graph operations

© 2018 Sebastian Koch, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Schlüsselwörter
supergraph, graph operations