(2019) Severín, Daniel Esteban; LIPIcs – Leibniz International Proceedings in Informatics
The Cockayne-Hedetniemi Domination Chain is a chain of inequalities between classic parameters
of graph theory: for a given graph G, ir(G) ≤ γ(G) ≤ ι(G) ≤ α(G) ≤ Γ(G) ≤ IR(G). These
parameters return the maximum/minimum cardinality of a set satisfying some property. However,
they can be generalized for graphs with weighted vertices where the objective is to maximize/minimize
the sum of weights of a set satisfying the same property, and the domination chain still holds for them.
In this work, the definition of these parameters as well as the chain is formalized in Coq/Ssreflect.