6533b838fe1ef96bd12a3c82
RESEARCH PRODUCT
Unification of Graphs and Relations in Mizar
Sebastian Kochsubject
binary relationUnificationgraph theoryApplied Mathematics020207 software engineering0102 computer and information sciences02 engineering and technologyMizar system68v2001 natural sciencesAlgebraComputational Mathematics010201 computation theory & mathematicsQA1-9390202 electrical engineering electronic engineering information engineering05c62MathematicsMathematicsofComputing_DISCRETEMATHEMATICSMathematicsdescription
Summary 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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2020-07-01 | Formalized Mathematics |